source: C-semantics @ 387

Name Size Rev Age Author Last Change
../
test 366   9 years campbell Make I/O type safe, removing a discrepancy between the executable and …
binary 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
8051-Memory 157   10 years campbell Make proposed memory spaces semantics more explicit.
Values.ma 27.9 KB 156   10 years campbell pdata support
SmallstepExec.ma 1.4 KB 25   10 years campbell Simplify the IO monad a little.
Smallstep.ma 27.8 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
root 32 bytes 254   9 years campbell Reset matita root.
README 4.8 KB 192   9 years campbell matita rev in README
Mem.ma 127.5 KB 190   9 years campbell Minor changes to work with current matita HEAD (r10998).
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
IOMonad.ma 8.4 KB 366   9 years campbell Make I/O type safe, removing a discrepancy between the executable and …
Integers.ma 80.6 KB 181   9 years campbell Sort out some axioms.
Globalenvs.ma 48.0 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
Floats.ma 2.6 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
extralib.ma 23.9 KB 181   9 years campbell Sort out some axioms.
Events.ma 10.8 KB 379   9 years campbell More whole execution equivalence - need ability to unfold cofixpoints …
Errors.ma 7.2 KB 250   9 years campbell Begin separating soundness from executable semantics.
Csyntax.ma 34.2 KB 255   9 years campbell Really restore matita root.
Csem.ma 78.3 KB 226   9 years campbell Some incomplete work on completeness of CexecIO wrt Csem. Features …
CostLabel.ma 51 bytes 177   9 years campbell Missing cost labels file.
Coqlib.ma 31.9 KB 173   9 years campbell Minor changes for newer versions of matita.
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
CexecIOcomplete.ma 44.3 KB 387   9 years campbell Sort out equality checking of types.
CexecIO.ma 69.8 KB 387   9 years campbell Sort out equality checking of types.
AST.ma 14.3 KB 156   10 years campbell pdata support
acc-0.1.spaces.patch 130.0 KB 292   9 years campbell Update acc 8051 syntax extension patch. Adds memory spaces to Clight …
Note: See TracBrowser for help on using the repository browser.