Changeset 1436 for Deliverables/D4.2-4.3

Timestamp:

Oct 21, 2011, 5:27:16 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/D4.2-4.3/reports/D4-2.tex (modified) (1 diff)

Deliverables/D4.2-4.3/reports/D4-2.tex

@@ -433 +433 @@
 These axiomatised components are found in the ERTL to LTL pass.
 
-It should be noted that these axiomatised components fall into the following pattern: whilst their implementation is complex, and their proof of correctness is difficult, we are able to quickly and easily verify that any answer that they provide is correct.
+It should be noted that these axiomatised components fall into the following pattern: whilst their implementation is complex, and their proof of correctness is difficult, we are able to quickly and easily verify that any answer that they provide is correct. Therefore, we plan to provide implementations in OCaml only,
+and to provide certified verifiers in Matita. At the moment, the implementation
+of the certified verifiers is left as future work.
 \item
 \textbf{A few non-computational proof obligations.}