source: C-semantics @ 235

Name Size Rev Age Author Last Change
../
8051-Memory 157   10 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   10 years campbell Patch to acc to parse 8051 memory spaces and output matita terms.
AST.ma 14.3 KB 156   10 years campbell pdata support
CexecIO.ma 39.0 KB 225   9 years campbell Missing case in cast.
CexecIOcomplete.ma 11.7 KB 226   9 years campbell Some incomplete work on completeness of CexecIO wrt Csem. Features …
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   10 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   10 years campbell pdata support
Note: See TracBrowser for help on using the repository browser.