source: C-semantics @ 189

Name Size Rev Age Author Last Change
../
test 156   10 years campbell pdata support
binary 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
8051-Memory 157   10 years campbell Make proposed memory spaces semantics more explicit.
Values.ma 27.9 KB 156   10 years campbell pdata support
SmallstepExec.ma 1.4 KB 25   10 years campbell Simplify the IO monad a little.
Smallstep.ma 27.8 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
root 32 bytes 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
README 4.9 KB 181   10 years campbell Sort out some axioms.
Mem.ma 127.3 KB 156   10 years campbell pdata support
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
IOMonad.ma 6.8 KB 189   10 years campbell Rework monad notation so that it is displayed well in proof mode.
Integers.ma 80.6 KB 181   10 years campbell Sort out some axioms.
Globalenvs.ma 48.0 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
Floats.ma 2.6 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
extralib.ma 23.9 KB 181   10 years campbell Sort out some axioms.
Events.ma 9.2 KB 175   10 years campbell Add cost labels, with the semantics that the label is added to the …
Errors.ma 7.1 KB 189   10 years campbell Rework monad notation so that it is displayed well in proof mode.
Csyntax.ma 34.2 KB 175   10 years campbell Add cost labels, with the semantics that the label is added to the …
Csem.ma 61.2 KB 175   10 years campbell Add cost labels, with the semantics that the label is added to the …
CostLabel.ma 51 bytes 177   10 years campbell Missing cost labels file.
Coqlib.ma 31.9 KB 173   10 years campbell Minor changes for newer versions of matita.
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
CexecIO.ma 38.8 KB 189   10 years campbell Rework monad notation so that it is displayed well in proof mode.
AST.ma 14.3 KB 156   10 years campbell pdata support
acc-0.1.spaces.patch 125.6 KB 160   10 years campbell Patch to acc to parse 8051 memory spaces and output matita terms.
Note: See TracBrowser for help on using the repository browser.