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

Name Size Rev Age Author Last Change
../
binary 400   9 years campbell Minor changes for the new version of matita.
test 479   9 years campbell Test of linked list insertion sort.
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 478   9 years campbell Prevent clashes between names in AST and other parts of the …
AST.ma 15.1 KB 483   9 years campbell Use pointer-specific "chunks" of memory for pointer loads and stores, …
Cexec.ma 32.9 KB 484   9 years campbell Separate out null values from integer zeros.
CexecComplete.ma 18.4 KB 484   9 years campbell Separate out null values from integer zeros.
CexecEquiv.ma 40.8 KB 399   9 years campbell Rearrange executable semantics a little.
CexecSound.ma 22.8 KB 484   9 years campbell Separate out null values from integer zeros.
compcert-1.7.1-matita.patch 18.4 KB 11   9 years campbell Fill in some axioms to aid executablity. Implement global variable …
Coqlib.ma 31.8 KB 473   9 years campbell Track changes in nlibrary list-theory.ma -> list.ma
CostLabel.ma 51 bytes 177   9 years campbell Missing cost labels file.
Csem.ma 78.2 KB 484   9 years campbell Separate out null values from integer zeros.
Csyntax.ma 34.0 KB 483   9 years campbell Use pointer-specific "chunks" of memory for pointer loads and stores, …
depends 1.5 KB 474   9 years campbell Reduce "include"s to reduce compilation time. (Will be undone when …
Errors.ma 7.2 KB 250   9 years campbell Begin separating soundness from executable semantics.
Events.ma 10.8 KB 478   9 years campbell Prevent clashes between names in AST and other parts of the …
extralib.ma 23.9 KB 400   9 years campbell Minor changes for the new version of matita.
Floats.ma 2.6 KB 3   9 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Globalenvs.ma 48.1 KB 480   9 years campbell "memory_space" to "region" replacement to match ocaml code
Integers.ma 80.6 KB 181   9 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   9 years campbell Fill in some axioms to aid executablity. Implement global variable …
Mem.ma 128.0 KB 484   9 years campbell Separate out null values from integer zeros.
README 5.5 KB 404   9 years campbell Update C-semantics README.
root 32 bytes 254   9 years campbell Reset matita root.
Smallstep.ma 27.8 KB 20   9 years campbell Add resumption monad based version of the executable semantics with …
SmallstepExec.ma 1.4 KB 469   9 years campbell Update work-in-progress file to match current development.
Values.ma 28.1 KB 484   9 years campbell Separate out null values from integer zeros.
Note: See TracBrowser for help on using the repository browser.