Skip to content

Latest commit

 

History

History
32 lines (20 loc) · 1.54 KB

README.md

File metadata and controls

32 lines (20 loc) · 1.54 KB
Raw

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.