source: C-semantics @ 397

Name Size Rev Age Author Last Change
../
8051-Memory 157   10 years campbell Make proposed memory spaces semantics more explicit.
binary 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
test 366   10 years campbell Make I/O type safe, removing a discrepancy between the executable and …
acc-0.1.spaces.patch 130.0 KB 292   10 years campbell Update acc 8051 syntax extension patch. Adds memory spaces to Clight …
AST.ma 14.3 KB 156   10 years campbell pdata support
CexecIO.ma 69.2 KB 389   10 years campbell Sort out minor inconsistency between semantics.
CexecIOcomplete.ma 47.1 KB 393   10 years campbell A few more details in D3.1.
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.9 KB 173   10 years campbell Minor changes for newer versions of matita.
CostLabel.ma 51 bytes 177   10 years campbell Missing cost labels file.
Csem.ma 78.3 KB 226   10 years campbell Some incomplete work on completeness of CexecIO wrt Csem. Features …
Csyntax.ma 34.2 KB 255   10 years campbell Really restore matita root.
Errors.ma 7.2 KB 250   10 years campbell Begin separating soundness from executable semantics.
Events.ma 10.8 KB 379   10 years campbell More whole execution equivalence - need ability to unfold cofixpoints …
extralib.ma 23.9 KB 181   10 years campbell Sort out some axioms.
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.6 KB 181   10 years campbell Sort out some axioms.
IOMonad.ma 8.4 KB 366   10 years campbell Make I/O type safe, removing a discrepancy between the executable and …
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Mem.ma 127.7 KB 391   10 years campbell Comment out daemon and its uses - we don't need the properties of the …
README 4.8 KB 192   10 years campbell matita rev in README
root 32 bytes 254   10 years campbell Reset matita root.
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.9 KB 156   10 years campbell pdata support
Note: See TracBrowser for help on using the repository browser.