|
../
|
|
CPP2011
|
|
1033
|
10 years
|
sacerdot |
ispelled & submitted
|
|
CPP2012-asm
|
|
2327
|
8 years
|
mulligan |
Fixed typos in paper highlighted by referees. More substantial …
|
|
CPP2012-policy
|
|
2099
|
9 years
|
boender |
- added reference to Intel dev manual
|
|
AbstractStatus.ma
|
2.0 KB
|
2770
|
8 years
|
mckinna |
WARNING: another big commit, touching many files in ASM/*.ma
This …
|
|
Arithmetic.ma
|
38.3 KB
|
2796
|
8 years
|
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
ASM.ma
|
36.4 KB
|
2767
|
8 years
|
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
ASMCosts.ma
|
36.7 KB
|
2832
|
8 years
|
sacerdot |
Added abstraction in front of cases daemon for code extraction.
|
|
ASMCostsSplit.ma
|
12.1 KB
|
2760
|
8 years
|
sacerdot |
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …
|
|
Assembly.ma
|
49.9 KB
|
2781
|
8 years
|
sacerdot |
One more computational daemon closed.
|
|
AssemblyProof.ma
|
62.0 KB
|
2516
|
8 years
|
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
|
AssemblyProofSplit.ma
|
119.7 KB
|
2516
|
8 years
|
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
|
AssemblyProofSplitSplit.ma
|
15.5 KB
|
2278
|
8 years
|
mulligan |
Half of JC case complete
|
|
BitVector.ma
|
7.1 KB
|
2782
|
8 years
|
sacerdot |
1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
|
|
BitVectorTrie.ma
|
26.6 KB
|
2767
|
8 years
|
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
BitVectorZ.ma
|
4.3 KB
|
2200
|
9 years
|
tranquil |
* updated joint semantics: generation of linear and graph semantics
* …
|
|
CodeMemory.ma
|
8.5 KB
|
2767
|
8 years
|
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
CostsProof.ma
|
32.3 KB
|
2760
|
8 years
|
sacerdot |
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …
|
|
Fetch.ma
|
32.5 KB
|
2770
|
8 years
|
mckinna |
WARNING: another big commit, touching many files in ASM/*.ma
This …
|
|
FoldStuff.ma
|
1.7 KB
|
1600
|
9 years
|
sacerdot |
utilities and ASM ported to the new standard library
|
|
I8051.ma
|
4.6 KB
|
2645
|
8 years
|
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
I8051bis.ma
|
125 bytes
|
1415
|
9 years
|
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
Interpret2.ma
|
1.6 KB
|
2875
|
8 years
|
sacerdot |
Pretty printing of object code integrated too.
A couple of axioms make …
|
|
Interpret.ma
|
60.3 KB
|
2770
|
8 years
|
mckinna |
WARNING: another big commit, touching many files in ASM/*.ma
This …
|
|
Policy.ma
|
35.4 KB
|
2771
|
8 years
|
sacerdot |
Some speed up in Policy.ma.
|
|
PolicyFront.ma
|
33.4 KB
|
2713
|
8 years
|
sacerdot |
PolicyFront?.ma repaired
|
|
PolicyStep.ma
|
59.8 KB
|
2714
|
8 years
|
sacerdot |
PolicyStep?.ma repaired
|
|
README
|
641 bytes
|
431
|
10 years
|
mulligan |
- README updated
- Test and DoTest? fixed to work on assembly_program
- …
|
|
Status.ma
|
36.3 KB
|
2770
|
8 years
|
mckinna |
WARNING: another big commit, touching many files in ASM/*.ma
This …
|
|
StatusProofs.ma
|
13.5 KB
|
2285
|
8 years
|
sacerdot |
1. duplicated code erased
2. POP case finished up to lemmas on …
|
|
StatusProofsSplit.ma
|
20.3 KB
|
2285
|
8 years
|
sacerdot |
1. duplicated code erased
2. POP case finished up to lemmas on …
|
|
Test.ma
|
92.8 KB
|
2284
|
8 years
|
sacerdot |
PUSH finished
|
|
Util.ma
|
41.5 KB
|
2700
|
8 years
|
sacerdot |
1. exponential function dropped in favour of standard library
2. …
|
|
UtilBranch.ma
|
2.4 KB
|
2702
|
8 years
|
sacerdot |
1. proof closed in ASM/UtilBranch
2. more passes integrated in the …
|
|
Vector.ma
|
34.9 KB
|
2286
|
8 years
|
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
WellLabeled.ma
|
6.8 KB
|
2710
|
8 years
|
sacerdot |
ASMCosts.ma repaired
|
