From 1bd9f4f3e71fa4a20f91ab74a1a5e6b6732eb0c1 Mon Sep 17 00:00:00 2001 From: Hannes Mehnert Date: Thu, 18 Jan 2018 15:14:43 +0100 Subject: [PATCH] add CFML --- Technology | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Technology b/Technology index 5d938c9..2bb9c20 100644 --- a/Technology +++ b/Technology @@ -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 direction is also possible: OCaml code can be translated into Coq definitions (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 OCaml runtime system, [their