source: C-semantics @ 145

Name Size Rev Age Author Last Change
../
8051-Memory 94   10 years sacerdot Minor comments.
binary 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
test 125   10 years campbell Unify memory space / pointer types. Implement global variable …
AST.ma 14.2 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
Cexec.ma 35.4 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
CexecIO.ma 36.2 KB 127   10 years campbell Allow the storage of pointers in suitably large integers.
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.3 KB 127   10 years campbell Allow the storage of pointers in suitably large integers.
Csyntax.ma 33.6 KB 127   10 years campbell Allow the storage of pointers in suitably large integers.
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.4 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
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.5 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
Note: See TracBrowser for help on using the repository browser.