source: C-semantics @ 85

Name Size Rev Age Author Last Change
../
8051-Memory 82   10 years campbell Start of document about impact of 8051 memory model on C.
binary 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
test 25   10 years campbell Simplify the IO monad a little.
root 32 bytes 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
SmallstepExec.ma 1.4 KB 25   10 years campbell Simplify the IO monad a little.
Floats.ma 2.6 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
README 4.6 KB 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
IOMonad.ma 5.8 KB 25   10 years campbell Simplify the IO monad a little.
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.
AST.ma 14.0 KB 24   10 years campbell Separate out IOMonad from the rest of the executable semantics. Start …
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
extralib.ma 22.2 KB 16   10 years campbell Add rest of the expressions to executable Clight semantics.
Values.ma 27.3 KB 14   10 years campbell Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.
Smallstep.ma 27.8 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
Coqlib.ma 31.8 KB 24   10 years campbell Separate out IOMonad from the rest of the executable semantics. Start …
Csyntax.ma 33.4 KB 24   10 years campbell Separate out IOMonad from the rest of the executable semantics. Start …
Cexec.ma 35.4 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
CexecIO.ma 38.0 KB 25   10 years campbell Simplify the IO monad a little.
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Globalenvs.ma 47.5 KB 24   10 years campbell Separate out IOMonad from the rest of the executable semantics. Start …
Csem.ma 59.2 KB 13   10 years campbell Minor syntactic changes.
Integers.ma 80.5 KB 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
Mem.ma 121.3 KB 24   10 years campbell Separate out IOMonad from the rest of the executable semantics. Start …
Note: See TracBrowser for help on using the repository browser.