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)
@1561
9 years
sacerdot
More dependent types to accomodate the statement.
(edit)
@1558
9 years
sacerdot
Snapshot before moving things to ASMCosts.ma.
(edit)
@1556
9 years
mulligan
submitting to avoid conflicts
(edit)
@1554
9 years
sacerdot
Major progress in the proof.
(edit)
@1549
9 years
mulligan
removed cruft from costsproof.ma file so claudio can work in parallel
(edit)
@1548
9 years
sacerdot
…
(edit)
@1544
9 years
sacerdot
StructuredTraces?
inhabited for object code.
(edit)
@1534
9 years
mulligan
committing my changes to interpret to prevent any further conflicts
(edit)
@1522
9 years
mulligan
changes to preamble and lin to asm pass, resolved conflict in interpret
(edit)
@1514
9 years
mulligan
changes from today. matita keeps dieing
(edit)
@1511
9 years
mulligan
proofs, added, changes to execute_1_0 function therefore required to …
(edit)
@1509
9 years
mulligan
i hate subtraction over the nats
(edit)
@1506
9 years
mulligan
changes to costs proof over weekend
(edit)
@1503
9 years
mulligan
inductive type complete
(edit)
@1502
9 years
mulligan
changes to inductive defn
(edit)
@1501
9 years
sacerdot
We must take in account the labelled_p predicate.
(edit)
@1500
9 years
sacerdot
Proof sketch for one of the two main proofs.
(edit)
@1499
9 years
mulligan
part way through main statement transcription
(add)
@1498
9 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