source: src @ 1971

Name Size Rev Age Author Last Change
../
ASM 1971   9 years sacerdot 1. Interpret.ma: we need to prove \sigma (execute_preinstruction …
Clight 1970   9 years garnier Work-in-progress: correction proof for the cast removal on expressions.
common 1964   9 years tranquil introduced as_label_of_cost and adapted accordingly. Equality of cost …
RTLabs 1960   9 years campbell Update RTLabs structured traces to make minor changes in definitions.
utilities 1949   9 years tranquil * lemma trace rel to eq flatten trace * some more properties of …
joint 1949   9 years tranquil * lemma trace rel to eq flatten trace * some more properties of …
Cminor 1884   9 years campbell Syntax changes to fit Paolo's commit.
RTL 1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
ERTL 1730   9 years sacerdot Minor changes while studying the proof.
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 …
acc-matita-printers.patch 7.1 KB 1633   9 years campbell Update Cminor pretty printer and examples.
TODO 606 bytes 1457   10 years sacerdot Bug fixed: when calling an internal function, the pc block is now set …
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 …
Note: See TracBrowser for help on using the repository browser.