source: C-semantics @ 124

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 124   10 years campbell Initial work on Clight semantics with 8051 memory spaces.
AST.ma 14.0 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 35.5 KB 124   10 years campbell Initial work on Clight semantics with 8051 memory spaces.
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.7 KB 124   10 years campbell Initial work on Clight semantics with 8051 memory spaces.
Csyntax.ma 33.7 KB 124   10 years campbell Initial work on Clight semantics with 8051 memory spaces.
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 47.6 KB 124   10 years campbell Initial work on Clight semantics with 8051 memory spaces.
Integers.ma 80.5 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.
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Mem.ma 127.4 KB 124   10 years campbell Initial work on Clight semantics with 8051 memory spaces.
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 28.0 KB 124   10 years campbell Initial work on Clight semantics with 8051 memory spaces.
Note: See TracBrowser for help on using the repository browser.