source: C-semantics @ 167

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 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.
AST.ma 14.3 KB 156   10 years campbell pdata support
Cexec.ma 35.4 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
CexecIO.ma 36.6 KB 156   10 years campbell pdata support
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.8 KB 24   10 years campbell Separate out IOMonad from the rest of the executable semantics. Start …
Csem.ma 60.4 KB 155   10 years campbell More sensible handling of integer types and pointer casts.
Csyntax.ma 33.8 KB 156   10 years campbell pdata support
Errors.ma 6.3 KB 4   10 years campbell Some experimental work on executable Clight semantics.
Events.ma 9.0 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
extralib.ma 22.2 KB 16   10 years campbell Add rest of the expressions to executable Clight semantics.
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.5 KB 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
IOMonad.ma 6.1 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Mem.ma 127.3 KB 156   10 years campbell pdata support
README 4.6 KB 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
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.