source: src/ASM/CostsProof.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @1658   9 years mulligan asm costs changes from today
(edit) @1650   9 years mulligan changes over the last couple of days: stuck due to matita producing …
(edit) @1648   9 years mulligan new version of utilities/monad.ma with typecheck command comented out
(edit) @1620   10 years sacerdot One of the mutual cases of the open proof is practically finished.
(edit) @1619   10 years sacerdot Major advancement.
(edit) @1587   10 years mulligan changes from today, including removing indexing of problematic …
(edit) @1581   10 years mulligan Dangling de Bruijn pointer when trying to propagate russell to set_arg_1
(edit) @1579   10 years mulligan Finished proof with simpler statement, making everything a lot nicer
(edit) @1577   10 years mulligan A lot more cases added to the proof at the bottom of …
(edit) @1576   10 years mulligan big changes to proofs, just two small cases remain and a few …
(edit) @1575   10 years mulligan Changes to specifications on execute functions
(edit) @1573   10 years mulligan more complicated than it appears :(
(edit) @1571   10 years mulligan small changes
(edit) @1570   10 years sacerdot Dependent type crazyness.
(edit) @1567   10 years mulligan more work on big proof, 2.5 cases left
(edit) @1564   10 years sacerdot Commit where we use a dependently typed version of bigops. I am now …
(edit) @1561   10 years sacerdot More dependent types to accomodate the statement.
(edit) @1558   10 years sacerdot Snapshot before moving things to ASMCosts.ma.
(edit) @1556   10 years mulligan submitting to avoid conflicts
(edit) @1554   10 years sacerdot Major progress in the proof.
(edit) @1549   10 years mulligan removed cruft from costsproof.ma file so claudio can work in parallel
(edit) @1548   10 years sacerdot
(edit) @1544   10 years sacerdot StructuredTraces? inhabited for object code.
(edit) @1534   10 years mulligan committing my changes to interpret to prevent any further conflicts
(edit) @1522   10 years mulligan changes to preamble and lin to asm pass, resolved conflict in interpret
(edit) @1514   10 years mulligan changes from today. matita keeps dieing
(edit) @1511   10 years mulligan proofs, added, changes to execute_1_0 function therefore required to …
(edit) @1509   10 years mulligan i hate subtraction over the nats
(edit) @1506   10 years mulligan changes to costs proof over weekend
(edit) @1503   10 years mulligan inductive type complete
(edit) @1502   10 years mulligan changes to inductive defn
(edit) @1501   10 years sacerdot We must take in account the labelled_p predicate.
(edit) @1500   10 years sacerdot Proof sketch for one of the two main proofs.
(edit) @1499   10 years mulligan part way through main statement transcription
(add) @1498   10 years mulligan added new file for proof that costs are preserved at asm level
Note: See TracRevisionLog for help on using the revision log.