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

Name Size Rev Age Author Last Change
../
binary 400   10 years campbell Minor changes for the new version of matita.
test 409   10 years campbell Update a couple of examples; put support for animation in its own file.
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.
depends 1.8 KB 409   10 years campbell Update a couple of examples; put support for animation in its own file.
Animation.ma 1.9 KB 409   10 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   10 years campbell Update C-semantics README.
Errors.ma 7.2 KB 250   10 years campbell Begin separating soundness from executable semantics.
IOMonad.ma 8.4 KB 366   10 years campbell Make I/O type safe, removing a discrepancy between the executable and …
Events.ma 10.8 KB 379   10 years campbell More whole execution equivalence - need ability to unfold cofixpoints …
AST.ma 14.3 KB 156   10 years campbell pdata support
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
CexecComplete.ma 18.5 KB 399   10 years campbell Rearrange executable semantics a little.
CexecSound.ma 22.7 KB 399   10 years campbell Rearrange executable semantics a little.
extralib.ma 23.9 KB 400   10 years campbell Minor changes for the new version of matita.
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.
Cexec.ma 33.0 KB 400   10 years campbell Minor changes for the new version of matita.
Csyntax.ma 34.2 KB 255   10 years campbell Really restore matita root.
CexecEquiv.ma 40.8 KB 399   10 years campbell Rearrange executable semantics a little.
Maps.ma 42.1 KB 11   10 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 …
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.7 KB 391   10 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   10 years campbell Update acc 8051 syntax extension patch. Adds memory spaces to Clight …
Note: See TracBrowser for help on using the repository browser.