source: C-semantics @ 245

Name Size Rev Age Author Last Change
../
8051-Memory 157   9 years campbell Make proposed memory spaces semantics more explicit.
binary 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
test 227   9 years campbell Update notation in an example.
acc-0.1.spaces.patch 125.6 KB 160   9 years campbell Patch to acc to parse 8051 memory spaces and output matita terms.
AST.ma 14.3 KB 156   9 years campbell pdata support
CexecIO.ma 43.6 KB 245   9 years campbell Some progress on whole-execution soundness.
CexecIOcomplete.ma 21.7 KB 239   9 years campbell More work on soundness and completeness of executable Clight semantics.
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Coqlib.ma 31.9 KB 173   9 years campbell Minor changes for newer versions of matita.
CostLabel.ma 51 bytes 177   9 years campbell Missing cost labels file.
Csem.ma 78.3 KB 226   9 years campbell Some incomplete work on completeness of CexecIO wrt Csem. Features …
Csyntax.ma 34.2 KB 175   9 years campbell Add cost labels, with the semantics that the label is added to the …
Errors.ma 7.1 KB 189   9 years campbell Rework monad notation so that it is displayed well in proof mode.
Events.ma 9.2 KB 175   9 years campbell Add cost labels, with the semantics that the label is added to the …
extralib.ma 23.9 KB 181   9 years campbell Sort out some axioms.
Floats.ma 2.6 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Globalenvs.ma 48.0 KB 125   9 years campbell Unify memory space / pointer types. Implement global variable …
Integers.ma 80.6 KB 181   9 years campbell Sort out some axioms.
IOMonad.ma 6.7 KB 211   9 years campbell Make io_inject definition more straightforward.
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Mem.ma 127.5 KB 190   9 years campbell Minor changes to work with current matita HEAD (r10998).
README 4.8 KB 192   9 years campbell matita rev in README
root 32 bytes 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Smallstep.ma 27.8 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
SmallstepExec.ma 1.4 KB 25   10 years campbell Simplify the IO monad a little.
Values.ma 27.9 KB 156   9 years campbell pdata support
Note: See TracBrowser for help on using the repository browser.