Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
source:
src
/
ASM
/
CostsProof.ma
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@1570
8 years
sacerdot
Dependent type crazyness.
(edit)
@1567
8 years
mulligan
more work on big proof, 2.5 cases left
(edit)
@1564
8 years
sacerdot
Commit where we use a dependently typed version of bigops. I am now …
(edit)
@1561
8 years
sacerdot
More dependent types to accomodate the statement.
(edit)
@1558
8 years
sacerdot
Snapshot before moving things to ASMCosts.ma.
(edit)
@1556
8 years
mulligan
submitting to avoid conflicts
(edit)
@1554
8 years
sacerdot
Major progress in the proof.
(edit)
@1549
8 years
mulligan
removed cruft from costsproof.ma file so claudio can work in parallel
(edit)
@1548
8 years
sacerdot
…
(edit)
@1544
8 years
sacerdot
StructuredTraces?
inhabited for object code.
(edit)
@1534
8 years
mulligan
committing my changes to interpret to prevent any further conflicts
(edit)
@1522
8 years
mulligan
changes to preamble and lin to asm pass, resolved conflict in interpret
(edit)
@1514
8 years
mulligan
changes from today. matita keeps dieing
(edit)
@1511
8 years
mulligan
proofs, added, changes to execute_1_0 function therefore required to …
(edit)
@1509
8 years
mulligan
i hate subtraction over the nats
(edit)
@1506
8 years
mulligan
changes to costs proof over weekend
(edit)
@1503
8 years
mulligan
inductive type complete
(edit)
@1502
8 years
mulligan
changes to inductive defn
(edit)
@1501
8 years
sacerdot
We must take in account the labelled_p predicate.
(edit)
@1500
8 years
sacerdot
Proof sketch for one of the two main proofs.
(edit)
@1499
8 years
mulligan
part way through main statement transcription
(add)
@1498
8 years
mulligan
added new file for proof that costs are preserved at asm level
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog