This commit is contained in:
Hannes Mehnert 2018-01-18 15:14:43 +01:00
parent aa07aa39a8
commit 1bd9f4f3e7

View file

@ -153,6 +153,9 @@ as demonstrated by [compcert](http://compcert.inria.fr/), a formally verified
optimizing C compiler, in order to be compiled and executed. The other optimizing C compiler, in order to be compiled and executed. The other
direction is also possible: OCaml code can be translated into Coq definitions direction is also possible: OCaml code can be translated into Coq definitions
(using [Coq of OCaml](https://github.com/clarus/coq-of-ocaml/)). (using [Coq of OCaml](https://github.com/clarus/coq-of-ocaml/)).
[CFML](http://www.chargueraud.org/softs/cfml/) is an ongoing research project
which enables us to prove properties about OCaml programs using the
[Coq](https://coq.inria.fr) proof assistant.
The National Cybersecurity Agency of France reviewed the implementation of the The National Cybersecurity Agency of France reviewed the implementation of the
OCaml runtime system, [their OCaml runtime system, [their