Uploaded at Nov 28 18:40:46 2020
Succesfully tested at Dec 2 06:10:00 2021

Curry Package verify

curry-verify - A Tool to Support the Verification of Curry Programs

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.

Installing the tool

The tool can be directly installed by the command

> cypm install verify

This installs the executable curry-verify in the bin directory of CPM.

Using the tool

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


Checkout with CPM:
cypm checkout verify 2.0.0
Package source:
verify-2.0.0.tar.gz [browse]
Source repository: