source: C-semantics @ 340

Name Size Rev Age Author Last Change
../
8051-Memory 157   10 years campbell Make proposed memory spaces semantics more explicit.
binary 15   11 years campbell Make some definitions more normalization friendly by a little 'nlet …
test 227   10 years campbell Update notation in an example.
root 32 bytes 254   10 years campbell Reset matita root.
CostLabel.ma 51 bytes 177   10 years campbell Missing cost labels file.
SmallstepExec.ma 1.4 KB 25   10 years campbell Simplify the IO monad a little.
Floats.ma 2.6 KB 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
README 4.8 KB 192   10 years campbell matita rev in README
Errors.ma 7.2 KB 250   10 years campbell Begin separating soundness from executable semantics.
IOMonad.ma 8.3 KB 252   10 years campbell Separate out soundness of exec_step from definition.
Events.ma 9.2 KB 175   10 years campbell Add cost labels, with the semantics that the label is added to the …
AST.ma 14.3 KB 156   10 years campbell pdata support
compcert-1.7.1-matita.patch 18.4 KB 11   11 years campbell Fill in some axioms to aid executablity. Implement global variable …
CexecIOcomplete.ma 20.4 KB 253   10 years campbell Update completeness proof for executable semantics with separate …
extralib.ma 23.9 KB 181   10 years campbell Sort out some axioms.
Smallstep.ma 27.8 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
Values.ma 27.9 KB 156   10 years campbell pdata support
Coqlib.ma 31.9 KB 173   10 years campbell Minor changes for newer versions of matita.
Csyntax.ma 34.2 KB 255   10 years campbell Really restore matita root.
Maps.ma 42.1 KB 11   11 years campbell Fill in some axioms to aid executablity. Implement global variable …
Globalenvs.ma 48.0 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
CexecIO.ma 65.1 KB 321   10 years campbell Soundness for reactive executions.
Csem.ma 78.3 KB 226   10 years campbell Some incomplete work on completeness of CexecIO wrt Csem. Features …
Integers.ma 80.6 KB 181   10 years campbell Sort out some axioms.
Mem.ma 127.5 KB 190   10 years campbell Minor changes to work with current matita HEAD (r10998).
acc-0.1.spaces.patch 130.0 KB 292   10 years campbell Update acc 8051 syntax extension patch. Adds memory spaces to Clight …
Note: See TracBrowser for help on using the repository browser.