This package contains the tool
curry-verify that supports the verification of Curry programs with the help of other theorem provers or proof assistants. Currently, only Agda is supported as a target language for verification (but more target languages may be supported in future releases). The ideas implemented by this tool are described in this paper:
S. Antoy, M. Hanus, and S. Libby: Proving non-deterministic computations in Agda. In Proc. of the 24th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2016), volume 234 of Electronic Proceedings in Theoretical Computer Science, pages 180–195. Open Publishing Association, 2017.
The tool can be directly installed by the command
> cypm install verify
This installs the executable
curry-verify in the bin directory of CPM.
If the bin directory of CPM (default:
~/.cpm/bin) is in your path, execute the tool with the module containing properties to be verified, e.g.,
> curry-verify -t agda -s choice Double