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

Name Size Rev Age Author Last Change
../
binary 400   10 years campbell Minor changes for the new version of matita.
test 479   10 years campbell Test of linked list insertion sort.
acc-0.1.spaces.patch 130.1 KB 416   10 years campbell Fix printing of switch statements as matita terms.
Animation.ma 1.9 KB 478   10 years campbell Prevent clashes between names in AST and other parts of the …
AST.ma 15.1 KB 483   10 years campbell Use pointer-specific "chunks" of memory for pointer loads and stores, …
Cexec.ma 33.1 KB 481   10 years campbell Tcomp_ptr should take the memory region and use that to calculate its size.
CexecComplete.ma 18.5 KB 481   10 years campbell Tcomp_ptr should take the memory region and use that to calculate its size.
CexecEquiv.ma 40.8 KB 399   10 years campbell Rearrange executable semantics a little.
CexecSound.ma 22.7 KB 481   10 years campbell Tcomp_ptr should take the memory region and use that to calculate its size.
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.8 KB 473   10 years campbell Track changes in nlibrary list-theory.ma -> list.ma
CostLabel.ma 51 bytes 177   10 years campbell Missing cost labels file.
Csem.ma 78.7 KB 481   10 years campbell Tcomp_ptr should take the memory region and use that to calculate its size.
Csyntax.ma 34.0 KB 483   10 years campbell Use pointer-specific "chunks" of memory for pointer loads and stores, …
depends 1.5 KB 474   10 years campbell Reduce "include"s to reduce compilation time. (Will be undone when …
Errors.ma 7.2 KB 250   10 years campbell Begin separating soundness from executable semantics.
Events.ma 10.8 KB 478   10 years campbell Prevent clashes between names in AST and other parts of the …
extralib.ma 23.9 KB 400   10 years campbell Minor changes for the new version of matita.
Floats.ma 2.6 KB 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Globalenvs.ma 48.1 KB 480   10 years campbell "memory_space" to "region" replacement to match ocaml code
Integers.ma 80.6 KB 181   10 years campbell Sort out some axioms.
IOMonad.ma 8.5 KB 411   10 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 128.0 KB 483   10 years campbell Use pointer-specific "chunks" of memory for pointer loads and stores, …
README 5.5 KB 404   10 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 469   10 years campbell Update work-in-progress file to match current development.
Values.ma 27.6 KB 483   10 years campbell Use pointer-specific "chunks" of memory for pointer loads and stores, …
Note: See TracBrowser for help on using the repository browser.