source: C-semantics @ 62

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