Impure: importing OCaml functions as non-deterministic ones.

The principle of this 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 correctness.

See further explanations and examples on ImpureDemo. This library is also part of Chamois CompCert.

Credits

Sylvain Boulmé.

Code Overview

• ImpMonads axioms of "impure computations" and some Coq models of these axioms.

• ImpConfig declares the Impure monad and defines its extraction.

• ImpCore defines notations for the Impure monad and a wlp_simplify tactic (to reason about Impure functions in a Hoare-logic style).

• ImpPrelude declares the data types exchanged with Impure oracles.

• ImpIO, ImpLoops, ImpHCons declare Impure oracles and define operators from these oracles. ImpExtern exports all these impure operators.

• ocaml/ subdirectory containing the OCaml implementations of Impure oracles.