source: src/ASM @ 2504

Name Size Rev Age Author Last Change
../
CPP2011 1033   8 years sacerdot ispelled & submitted
CPP2012-asm 2327   7 years mulligan Fixed typos in paper highlighted by referees. More substantial …
CPP2012-policy 2099   7 years boender - added reference to Intel dev manual
AbstractStatus.ma 2.0 KB 2498   7 years mckinna Refactor: Typedefs object_code and costlabel_map lifted out from …
Arithmetic.ma 36.3 KB 2311   7 years garnier Some more cleaning of switchRemoval …
ASM.ma 32.5 KB 2316   7 years boender - committed temporary version: true version has to wait until I …
ASMCosts.ma 35.3 KB 2504   7 years mckinna More refactoring to support the tidied up compiler.ma
ASMCostsSplit.ma 12.2 KB 2504   7 years mckinna More refactoring to support the tidied up compiler.ma
Assembly.ma 48.2 KB 2498   7 years mckinna Refactor: Typedefs object_code and costlabel_map lifted out from …
AssemblyProof.ma 62.0 KB 2498   7 years mckinna Refactor: Typedefs object_code and costlabel_map lifted out from …
AssemblyProofSplit.ma 119.7 KB 2498   7 years mckinna Refactor: Typedefs object_code and costlabel_map lifted out from …
AssemblyProofSplitSplit.ma 15.5 KB 2278   7 years mulligan Half of JC case complete
BitVector.ma 7.7 KB 2126   7 years sacerdot Proof improved (for case 3) + new proof (for case 11)
BitVectorTrie.ma 25.7 KB 2028   7 years boender - bugfix to Assembly (forgotten sigma) - added …
BitVectorZ.ma 4.3 KB 2200   7 years tranquil * updated joint semantics: generation of linear and graph semantics * …
Char.ma 76 bytes 697   9 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
CostsProof.ma 32.9 KB 2498   7 years mckinna Refactor: Typedefs object_code and costlabel_map lifted out from …
Erase.ma 3.5 KB 1600   8 years sacerdot utilities and ASM ported to the new standard library
Fetch.ma 32.5 KB 2498   7 years mckinna Refactor: Typedefs object_code and costlabel_map lifted out from …
FoldStuff.ma 1.7 KB 1600   8 years sacerdot utilities and ASM ported to the new standard library
I8051.ma 4.7 KB 2286   7 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
I8051bis.ma 125 bytes 1415   8 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
Interpret2.ma 2.3 KB 2498   7 years mckinna Refactor: Typedefs object_code and costlabel_map lifted out from …
Interpret.ma 58.9 KB 2504   7 years mckinna More refactoring to support the tidied up compiler.ma
Policy.ma 35.4 KB 2318   7 years boender - now it compiles
PolicyFront.ma 32.3 KB 2318   7 years boender - now it compiles
PolicyStep.ma 59.3 KB 2317   7 years boender - small changes to make things compile
README 641 bytes 431   9 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 38.4 KB 2316   7 years boender - committed temporary version: true version has to wait until I …
StatusProofs.ma 13.5 KB 2285   7 years sacerdot 1. duplicated code erased 2. POP case finished up to lemmas on …
StatusProofsSplit.ma 20.3 KB 2285   7 years sacerdot 1. duplicated code erased 2. POP case finished up to lemmas on …
String.ma 90 bytes 1599   8 years sacerdot Start of merging of stuff into the standard library of Matita.
Test.ma 92.8 KB 2284   7 years sacerdot PUSH finished
Util.ma 41.7 KB 2314   7 years campbell Move generic definitions from recent commit to appropriate places.
UtilBranch.ma 2.2 KB 1946   8 years sacerdot \snd half_add => add everywhere
Vector.ma 34.9 KB 2286   7 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
WellLabeled.ma 6.9 KB 2032   7 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
Note: See TracBrowser for help on using the repository browser.