source: Deliverables/D3.1/C-semantics @ 432

Name Size Rev Age Author Last Change
../
binary 400   9 years campbell Minor changes for the new version of matita.
test 415   9 years campbell A couple of amusing examples.
acc-0.1.spaces.patch 130.1 KB 416   9 years campbell Fix printing of switch statements as matita terms.
Animation.ma 1.9 KB 409   9 years campbell Update a couple of examples; put support for animation in its own file.
AST.ma 14.3 KB 156   10 years campbell pdata support
Cexec.ma 33.0 KB 400   9 years campbell Minor changes for the new version of matita.
CexecComplete.ma 18.5 KB 399   9 years campbell Rearrange executable semantics a little.
CexecEquiv.ma 40.8 KB 399   9 years campbell Rearrange executable semantics a little.
CexecSound.ma 22.7 KB 399   9 years campbell Rearrange executable semantics a little.
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.
depends 1.8 KB 409   9 years campbell Update a couple of examples; put support for animation in its own file.
Errors.ma 7.2 KB 250   10 years campbell Begin separating soundness from executable semantics.
Events.ma 10.8 KB 379   9 years campbell More whole execution equivalence - need ability to unfold cofixpoints …
extralib.ma 23.9 KB 400   9 years campbell Minor changes for the new version of matita.
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.5 KB 411   9 years campbell Note associativity of IOMonad, subject to extensionality.
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   9 years campbell Comment out daemon and its uses - we don't need the properties of the …
README 5.5 KB 404   9 years campbell Update C-semantics 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.