source:
C-semantics
@
20
Name | Size | Rev | Age | Author | Last Change |
---|---|---|---|---|---|
../ | |||||
binary | 15 | 11 years | Make some definitions more normalization friendly by a little 'nlet … | ||
test | 20 | 11 years | Add resumption monad based version of the executable semantics with … | ||
AST.ma | 13.9 KB | 10 | 11 years | Add binary arithmetic libraries, use for integers and identifiers (but … | |
Cexec.ma | 35.4 KB | 20 | 11 years | Add resumption monad based version of the executable semantics with … | |
CexecIO.ma | 42.7 KB | 20 | 11 years | Add resumption monad based version of the executable semantics with … | |
compcert-1.7.1-matita.patch | 18.4 KB | 11 | 11 years | Fill in some axioms to aid executablity. Implement global variable … | |
Coqlib.ma | 31.7 KB | 10 | 11 years | Add binary arithmetic libraries, use for integers and identifiers (but … | |
Csem.ma | 59.2 KB | 13 | 11 years | Minor syntactic changes. | |
Csyntax.ma | 30.0 KB | 4 | 11 years | Some experimental work on executable Clight semantics. | |
Errors.ma | 6.3 KB | 4 | 11 years | Some experimental work on executable Clight semantics. | |
Events.ma | 9.0 KB | 3 | 11 years | Import work-in-progress port of the CompCert? C semantics to matita. | |
extralib.ma | 22.2 KB | 16 | 11 years | Add rest of the expressions to executable Clight semantics. | |
Floats.ma | 2.6 KB | 3 | 11 years | Import work-in-progress port of the CompCert? C semantics to matita. | |
Globalenvs.ma | 42.6 KB | 3 | 11 years | Import work-in-progress port of the CompCert? C semantics to matita. | |
Integers.ma | 80.5 KB | 15 | 11 years | Make some definitions more normalization friendly by a little 'nlet … | |
Maps.ma | 42.1 KB | 11 | 11 years | Fill in some axioms to aid executablity. Implement global variable … | |
Mem.ma | 121.3 KB | 15 | 11 years | Make some definitions more normalization friendly by a little 'nlet … | |
README | 4.6 KB | 15 | 11 years | Make some definitions more normalization friendly by a little 'nlet … | |
root | 32 bytes | 3 | 11 years | Import work-in-progress port of the CompCert? C semantics to matita. | |
Smallstep.ma | 27.8 KB | 20 | 11 years | Add resumption monad based version of the executable semantics with … | |
Values.ma | 27.3 KB | 14 | 11 years | Make Integers.ma respect bounds again, and reenable the rest of Mem.ma. |
Note: See TracBrowser
for help on using the repository browser.