source: C-semantics @ 251

Name Size Rev Age Author Last Change
../
binary 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
8051-Memory 157   10 years campbell Make proposed memory spaces semantics more explicit.
test 227   10 years campbell Update notation in an example.
Floats.ma 2.6 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
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.
Globalenvs.ma 48.0 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
AST.ma 14.3 KB 156   10 years campbell pdata support
Values.ma 27.9 KB 156   10 years campbell pdata support
acc-0.1.spaces.patch 125.6 KB 160   10 years campbell Patch to acc to parse 8051 memory spaces and output matita terms.
Coqlib.ma 31.9 KB 173   10 years campbell Minor changes for newer versions of matita.
Events.ma 9.2 KB 175   10 years campbell Add cost labels, with the semantics that the label is added to the …
CostLabel.ma 51 bytes 177   10 years campbell Missing cost labels file.
extralib.ma 23.9 KB 181   10 years campbell Sort out some axioms.
Integers.ma 80.6 KB 181   10 years campbell Sort out some axioms.
Mem.ma 127.5 KB 190   10 years campbell Minor changes to work with current matita HEAD (r10998).
README 4.8 KB 192   10 years campbell matita rev in README
Csem.ma 78.3 KB 226   10 years campbell Some incomplete work on completeness of CexecIO wrt Csem. Features …
CexecIOcomplete.ma 21.7 KB 250   10 years campbell Begin separating soundness from executable semantics.
Errors.ma 7.2 KB 250   10 years campbell Begin separating soundness from executable semantics.
root 34 bytes 250   10 years campbell Begin separating soundness from executable semantics.
CexecIO.ma 55.5 KB 251   10 years campbell Separate out soundness of exec_expr from definition.
Csyntax.ma 34.2 KB 251   10 years campbell Separate out soundness of exec_expr from definition.
IOMonad.ma 7.2 KB 251   10 years campbell Separate out soundness of exec_expr from definition.
Note: See TracBrowser for help on using the repository browser.