package coq-paramcoq

You can search for identifiers within the package.

in-package search v0.2.0

Plugin for generating parametricity statements to perform refinement proofs

Install

Dune Dependency

github.com Edit opam file Versions (26)

Authors

Maintainers

P

Pierre Roux <pierre.roux@onera.fr>

Sources

v1.1.2+coq8.11.tar.gz

sha256=d737aefb6a0845459ac1ba9c1b1617dd33c1c4bc3f8fa82568e6f4d32506dc65

Description

The plugin is still in an experimental state. It is not very user friendly (lack of good error messages) and still contains bugs. But is useable enough to "translate" a large chunk of standard library.

Published: 31 Jan 2020

Dependencies (3)

ocamlfind build
ocaml
coq >= "8.11" & < "8.12~"

Dev Dependencies

None

Used by (4)

coq-addition-chains < "0.5"
coq-coqeal < "1.1.0"
coq-monae >= "0.1.1" & < "0.4"
coq-validsdp < "1.0.4"

Conflicts