source: src @ 1877

Name Size Rev Age Author Last Change
../
ASM 1870   9 years boender - changed sigma00 in Assembly to use foldl_strong + proved invariants …
Clight 1876   9 years campbell Update Cexec soundness proof. Change finishes_with predicate to …
Cminor 1874   9 years campbell First cut at using back-end memory model throughout. Note the …
common 1876   9 years campbell Update Cexec soundness proof. Change finishes_with predicate to …
ERTL 1730   9 years sacerdot Minor changes while studying the proof.
joint 1874   9 years campbell First cut at using back-end memory model throughout. Note the …
LIN 1601   10 years sacerdot Files ported to new version of the standard library.
LTL 1515   10 years campbell Add type of maps on positive binary numbers, and use them for …
RTL 1644   9 years tranquil minor changes
RTLabs 1877   9 years campbell Update RTLabs structured traces for typed binops and new memory model.
utilities 1648   9 years mulligan new version of utilities/monad.ma with typecheck command comented out
acc-matita-printers.patch 7.1 KB 1633   9 years campbell Update Cminor pretty printer and examples.
CHANGES 3.4 KB 1388   10 years sacerdot fetch_result implemented for ERTL. This required a different …
root 26 bytes 703   10 years sacerdot lib is now the default standard library (after commit 11216 in …
TODO 606 bytes 1457   10 years sacerdot Bug fixed: when calling an internal function, the pc block is now set …
Note: See TracBrowser for help on using the repository browser.