source: C-semantics @ 185

Name Size Rev Age Author Last Change
../
binary 15   11 years campbell Make some definitions more normalization friendly by a little 'nlet …
test 156   11 years campbell pdata support
8051-Memory 157   11 years campbell Make proposed memory spaces semantics more explicit.
Floats.ma 2.6 KB 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
root 32 bytes 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Errors.ma 6.3 KB 4   11 years campbell Some experimental work on executable Clight semantics.
compcert-1.7.1-matita.patch 18.4 KB 11   11 years campbell Fill in some axioms to aid executablity. Implement global variable …
Maps.ma 42.1 KB 11   11 years campbell Fill in some axioms to aid executablity. Implement global variable …
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.
Globalenvs.ma 48.0 KB 125   11 years campbell Unify memory space / pointer types. Implement global variable …
IOMonad.ma 6.1 KB 125   11 years campbell Unify memory space / pointer types. Implement global variable …
AST.ma 14.3 KB 156   11 years campbell pdata support
Mem.ma 127.3 KB 156   11 years campbell pdata support
Values.ma 27.9 KB 156   11 years campbell pdata support
acc-0.1.spaces.patch 125.6 KB 160   11 years campbell Patch to acc to parse 8051 memory spaces and output matita terms.
Coqlib.ma 31.9 KB 173   11 years campbell Minor changes for newer versions of matita.
CexecIO.ma 38.7 KB 175   11 years campbell Add cost labels, with the semantics that the label is added to the …
Csem.ma 61.2 KB 175   11 years campbell Add cost labels, with the semantics that the label is added to the …
Csyntax.ma 34.2 KB 175   11 years campbell Add cost labels, with the semantics that the label is added to the …
Events.ma 9.2 KB 175   11 years campbell Add cost labels, with the semantics that the label is added to the …
CostLabel.ma 51 bytes 177   11 years campbell Missing cost labels file.
extralib.ma 23.9 KB 181   11 years campbell Sort out some axioms.
Integers.ma 80.6 KB 181   11 years campbell Sort out some axioms.
README 4.9 KB 181   11 years campbell Sort out some axioms.
Note: See TracBrowser for help on using the repository browser.