ImpureDemo: importing OCaml functions as non-deterministic ones.
The principle of the
Impure library is to encode the type
A -> B
of an OCaml function as a type
A -> ?? B in Coq, where
?? B is the
type of an axiomatized monad that can be interpreted as
B -> Prop.
In other word, this encoding abstracts an OCaml function as a function
returning a postcondition on its possible results (ie a relation
between its parameter and its result). Side-effects are simply
ignored. And reasoning on such a function is only possible in partial
A major feature of this cooperation between Coq and OCaml typechecker
is to provide very simple
about polymorphic OCaml functions. They correspond here to prove, by
reasoning only on their type, that these functions preserve some
invariants. As an example, we prove the partial correctness of a
generic memoizing fixpoint operator: see
rec_correct lemma at the
end of ImpLoops. This lemma is applied
in FibExample to prove the partial correctness
of a memoized version of the naive Fibonacci function. However,
currently, the soundness of these parametric proofs is still a
ocaml. Tested with versions >= 4.05 and <= 4.07.0. (But other versions should work too).
ocamlbuild. Tested with version 0.12.0. (But other versions should work too).
coq. Tested with versions >= 8.7.2 and <= 8.8.2. Here, other versions are likely to not work !
After cloning, just change directory for a building directory (see below), and run
coq_src/ contains the Coq sources. Other directories aims to build examples of binaries.