source: src/ASM @ 1956

Name Size Rev Age Author Last Change
../
CPP2011 1033   9 years sacerdot ispelled & submitted
SEFM2012 1889   9 years boender - some pages of article
AbstractStatus.ma 2.0 KB 1944   8 years sacerdot common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
Arithmetic.ma 17.7 KB 1955   8 years mulligan Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …
ASM.ma 9.0 KB 1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
ASMCosts.ma 35.4 KB 1938   8 years sacerdot Definitions moved to the right places, now everything compiles again.
ASMCostsSplit.ma 11.6 KB 1946   8 years sacerdot \snd half_add => add everywhere
Assembly.ma 56.2 KB 1948   8 years mulligan Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …
AssemblyProof.ma 72.2 KB 1955   8 years mulligan Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …
AssemblyProofSplit.ma 20.3 KB 1952   8 years sacerdot AssemblyProof? splitted.
BitVector.ma 6.7 KB 1928   8 years mulligan Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
BitVectorTrie.ma 24.3 KB 1931   8 years boender - added latest bvt alias - temporary "cases daemon" commit of new …
BitVectorZ.ma 4.0 KB 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
Char.ma 76 bytes 697   10 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
CostsProof.ma 32.5 KB 1935   8 years mulligan Generalized some lemma in ASM/CostsProof.ma to work on abstract …
Erase.ma 3.5 KB 1600   9 years sacerdot utilities and ASM ported to the new standard library
Fetch.ma 23.5 KB 1946   8 years sacerdot \snd half_add => add everywhere
FoldStuff.ma 1.7 KB 1600   9 years sacerdot utilities and ASM ported to the new standard library
I8051.ma 6.9 KB 1635   9 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
I8051bis.ma 125 bytes 1415   9 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
Interpret2.ma 2.3 KB 1606   9 years sacerdot Porting to last library of Matita.
Interpret.ma 47.0 KB 1951   8 years sacerdot Bug with overloaded names in the context.
Policy.ma 92.6 KB 1956   8 years boender - finished proof of lemma (where auto does strange things again)
README 641 bytes 431   10 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 40.3 KB 1946   8 years sacerdot \snd half_add => add everywhere
StatusProofs.ma 13.2 KB 1710   9 years mulligan changes from friday afternoon
String.ma 90 bytes 1599   9 years sacerdot Start of merging of stuff into the standard library of Matita.
Util.ma 32.8 KB 1937   8 years boender - filled in some of the gaps in the proof of Policy - reverted …
UtilBranch.ma 2.2 KB 1946   8 years sacerdot \snd half_add => add everywhere
Vector.ma 17.8 KB 1908   8 years fguidi notation fixup following last commit of matita we shifted the levels …
WellLabeled.ma 6.9 KB 1494   9 years mulligan changes to get everything compiling again
Note: See TracBrowser for help on using the repository browser.