diff options
Diffstat (limited to 'kvx/abstractbb/Impure/README.md')
| -rw-r--r-- | kvx/abstractbb/Impure/README.md | 31 |
1 files changed, 0 insertions, 31 deletions
diff --git a/kvx/abstractbb/Impure/README.md b/kvx/abstractbb/Impure/README.md deleted file mode 100644 index 2b19d14a..00000000 --- a/kvx/abstractbb/Impure/README.md +++ /dev/null @@ -1,31 +0,0 @@ -# `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](https://github.com/boulme/ImpureDemo). - -## Credits - -[Sylvain Boulmé](mailto:Sylvain.Boulme@univ-grenoble-alpes.fr). - -## Code Overview - -- [ImpMonads](ImpMonads.v) axioms of "impure computations" and some Coq models of these axioms. - -- [ImpConfig](ImpConfig.v) declares the `Impure` monad and defines its extraction. - -- [ImpCore](ImpCore.v) defines notations for the `Impure` monad and a `wlp_simplify` tactic (to reason about `Impure` functions in a Hoare-logic style). - -- [ImpPrelude](ImpPrelude.v) declares the data types exchanged with `Impure` oracles. - -- [ImpIO](ImpIO.v), [ImpLoops](ImpLoops.v), [ImpHCons](ImpHCons.v) declare `Impure` oracles and define operators from these oracles. - [ImpExtern](ImpExtern.v) exports all these impure operators. - -- [ocaml/](ocaml/) subdirectory containing the OCaml implementations of `Impure` oracles. - |