Ignore:
Timestamp:
Feb 6, 2013, 11:28:32 PM (6 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec.tex

    r2634 r2635  
    111111
    112112In this paper we present a formalisation in the Matita interactive theorem
    113 prover of a generic version of the simulation proof required for unstructured
     113prover~\cite{matita1,matita2} of a generic version of the simulation proof required for unstructured
    114114languages. All back-end languages of the CerCo compiler are unstructured
    115115languages, so the proof covers half of the correctness of the compiler.
Note: See TracChangeset for help on using the changeset viewer.