source: C-semantics @ 295

Name Size Rev Age Author Last Change
../
8051-Memory 157   11 years campbell Make proposed memory spaces semantics more explicit.
binary 15   11 years campbell Make some definitions more normalization friendly by a little 'nlet …
test 227   11 years campbell Update notation in an example.
acc-0.1.spaces.patch 130.0 KB 292   11 years campbell Update acc 8051 syntax extension patch. Adds memory spaces to Clight …
AST.ma 14.3 KB 156   11 years campbell pdata support
CexecIO.ma 63.7 KB 295   11 years campbell Soundness of terminating whole program execution.
CexecIOcomplete.ma 20.4 KB 253   11 years campbell Update completeness proof for executable semantics with separate …
compcert-1.7.1-matita.patch 18.4 KB 11   11 years campbell Fill in some axioms to aid executablity. Implement global variable …
Coqlib.ma 31.9 KB 173   11 years campbell Minor changes for newer versions of matita.
CostLabel.ma 51 bytes 177   11 years campbell Missing cost labels file.
Csem.ma 78.3 KB 226   11 years campbell Some incomplete work on completeness of CexecIO wrt Csem. Features …
Csyntax.ma 34.2 KB 255   11 years campbell Really restore matita root.
Errors.ma 7.2 KB 250   11 years campbell Begin separating soundness from executable semantics.
Events.ma 9.2 KB 175   11 years campbell Add cost labels, with the semantics that the label is added to the …
extralib.ma 23.9 KB 181   11 years campbell Sort out some axioms.
Floats.ma 2.6 KB 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Globalenvs.ma 48.0 KB 125   11 years campbell Unify memory space / pointer types. Implement global variable …
Integers.ma 80.6 KB 181   11 years campbell Sort out some axioms.
IOMonad.ma 8.3 KB 252   11 years campbell Separate out soundness of exec_step from definition.
Maps.ma 42.1 KB 11   11 years campbell Fill in some axioms to aid executablity. Implement global variable …
Mem.ma 127.5 KB 190   11 years campbell Minor changes to work with current matita HEAD (r10998).
README 4.8 KB 192   11 years campbell matita rev in README
root 32 bytes 254   11 years campbell Reset matita root.
Smallstep.ma 27.8 KB 20   11 years campbell Add resumption monad based version of the executable semantics with …
SmallstepExec.ma 1.4 KB 25   11 years campbell Simplify the IO monad a little.
Values.ma 27.9 KB 156   11 years campbell pdata support
Note: See TracBrowser for help on using the repository browser.