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

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.
root 32 bytes 254   9 years campbell Reset matita root.
CostLabel.ma 51 bytes 177   9 years campbell Missing cost labels file.
SmallstepExec.ma 1.4 KB 25   9 years campbell Simplify the IO monad a little.
depends 1.8 KB 409   9 years campbell Update a couple of examples; put support for animation in its own file.
Animation.ma 1.9 KB 409   9 years campbell Update a couple of examples; put support for animation in its own file.
Floats.ma 2.6 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
README 5.5 KB 404   9 years campbell Update C-semantics README.
Errors.ma 7.2 KB 250   9 years campbell Begin separating soundness from executable semantics.
IOMonad.ma 8.5 KB 411   9 years campbell Note associativity of IOMonad, subject to extensionality.
Events.ma 10.8 KB 379   9 years campbell More whole execution equivalence - need ability to unfold cofixpoints …
AST.ma 14.3 KB 156   9 years campbell pdata support
compcert-1.7.1-matita.patch 18.4 KB 11   9 years campbell Fill in some axioms to aid executablity. Implement global variable …
CexecComplete.ma 18.5 KB 399   9 years campbell Rearrange executable semantics a little.
CexecSound.ma 22.7 KB 399   9 years campbell Rearrange executable semantics a little.
extralib.ma 23.9 KB 400   9 years campbell Minor changes for the new version of matita.
Smallstep.ma 27.8 KB 20   9 years campbell Add resumption monad based version of the executable semantics with …
Values.ma 27.9 KB 156   9 years campbell pdata support
Coqlib.ma 31.9 KB 173   9 years campbell Minor changes for newer versions of matita.
Cexec.ma 33.0 KB 400   9 years campbell Minor changes for the new version of matita.
Csyntax.ma 34.2 KB 255   9 years campbell Really restore matita root.
CexecEquiv.ma 40.8 KB 399   9 years campbell Rearrange executable semantics a little.
Maps.ma 42.1 KB 11   9 years campbell Fill in some axioms to aid executablity. Implement global variable …
Globalenvs.ma 48.0 KB 125   9 years campbell Unify memory space / pointer types. Implement global variable …
Csem.ma 78.3 KB 226   9 years campbell Some incomplete work on completeness of CexecIO wrt Csem. Features …
Integers.ma 80.6 KB 181   9 years campbell Sort out some axioms.
Mem.ma 127.7 KB 391   9 years campbell Comment out daemon and its uses - we don't need the properties of the …
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.