Changeset 1441 for Deliverables


Ignore:
Timestamp:
Oct 21, 2011, 5:51:07 PM (9 years ago)
Author:
mulligan
Message:

small change

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-2.tex

    r1440 r1441  
    427427These axiomatised components are found in the ERTL to LTL pass.
    428428
    429 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,
    430 and to provide certified verifiers in Matita.
     429It 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.
     430Therefore, we plan to provide implementations in OCaml only, and to provide certified verifiers in Matita.
    431431At the moment, the implementation of the certified verifiers is left as future work.
    432432\item
Note: See TracChangeset for help on using the changeset viewer.