Timeline


and

Jun 8, 2011:

6:15 PM Changeset [907] by boender
- added quadruples to Util - start of implementation of new jump …
6:12 PM Changeset [906] by sacerdot
6:07 PM Changeset [905] by mulligan
work from today
5:53 PM Changeset [904] by sacerdot
Cleanup.
5:53 PM Changeset [903] by sacerdot
Statement of new main lemma (as axiom).
5:28 PM Changeset [902] by sacerdot
Cleanup.
5:27 PM Changeset [901] by sacerdot
Second main lemma proved.
2:24 PM Changeset [900] by sacerdot
New implementation of flatten was bugged: fixed.
2:17 PM Changeset [899] by mulligan
changed defn. of flatten
1:14 PM Changeset [898] by campbell
Update pretty printers and examples.
10:59 AM Changeset [897] by sacerdot
Proof completed, fetch and assembly are mutual inverses.
10:38 AM Changeset [896] by sacerdot
Proof finished (but ugly) :-)
10:30 AM Changeset [895] by sacerdot
Fetch function fixed: alla AJMPS were ACALL (and the other way around) …
10:09 AM Changeset [894] by sacerdot
Bug more evident.
9:46 AM PublicationVenues edited by mulligan
(diff)

Jun 7, 2011:

5:32 PM Changeset [893] by sacerdot
Cleanup.
5:28 PM Changeset [892] by sacerdot
First fundamental lemma almost finished.
4:53 PM Changeset [891] by campbell
Revise proofs affected by recent matita change.
2:56 AM Changeset [890] by sacerdot
Better statement, begin of uniform proof.

Jun 6, 2011:

11:07 PM Changeset [889] by sacerdot
Minor changes because of the new, weaker (but much faster) delift.
4:28 PM Changeset [888] by campbell
Use simplified conditionals in RTLabs, following the prototype.
3:55 PM Changeset [887] by campbell
Start bringing RTLabs into line with the prototype compiler: - a …
1:27 PM Changeset [886] by campbell
Put types into parameter and variable lists in Cminor. Temporarily …

Jun 5, 2011:

2:04 AM Changeset [885] by sacerdot
Proof almost finished, but rewritings are extremely slow.

Jun 4, 2011:

6:16 PM Changeset [884] by sacerdot

Jun 3, 2011:

6:36 PM Changeset [883] by sacerdot
Merged done well.
5:35 PM Changeset [882] by campbell
Fix up fragile proofs for current version of matita.
5:35 PM Changeset [881] by campbell
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.
5:35 PM Changeset [880] by campbell
Add type information into Cminor. As a result, the Clight to Cminor …
5:35 PM Changeset [879] by campbell
Refine "AST" types to include size/signedness information.
5:35 PM Changeset [878] by campbell
Removal of manually inserted record projections.
4:11 PM Changeset [877] by mulligan
work from today
4:03 PM Changeset [876] by sacerdot
11:21 AM Changeset [875] by sacerdot
10:13 AM Changeset [874] by sacerdot
Tactics no longer works.

Jun 2, 2011:

5:47 PM Changeset [873] by sacerdot
Script improved. Maybe this requires an svn up of Matita.

Jun 1, 2011:

5:32 PM Changeset [872] by mulligan
changes from today, need investigation of reduction machine

May 31, 2011:

6:05 PM Changeset [871] by sacerdot
5:54 PM Changeset [870] by mulligan
more changes
5:28 PM Changeset [869] by sacerdot
More progress.
5:28 PM Changeset [868] by mulligan
more changes
5:01 PM Changeset [867] by mulligan
changes to assembly proof
3:03 PM Changeset [866] by sacerdot
Significant improvement in the proof.
11:45 AM Changeset [865] by sacerdot
Renaming.
11:27 AM Changeset [864] by mulligan
resolved conflict
2:56 AM Changeset [863] by sacerdot
Yet another fix to the statement.
2:33 AM Changeset [862] by sacerdot
1:39 AM Changeset [861] by sacerdot
Statement of the lemma fixed (again!) Some preliminary work on …

May 30, 2011:

6:43 PM Changeset [860] by sacerdot
Progress in the proof.
6:38 PM Changeset [859] by mulligan
more added
4:43 PM Changeset [858] by sacerdot
If then else notation improved.
4:37 PM Changeset [857] by sacerdot
Notations.
1:44 PM Changeset [856] by sacerdot
1. if_then_else is now a notation for match with (to allow Russell to …

May 27, 2011:

6:11 PM Changeset [855] by mulligan
changes from today
5:13 PM Changeset [854] by mulligan
commit to avoid conflicts
1:58 PM Changeset [853] by sacerdot
1:26 PM Changeset [852] by mulligan
foldl_strong outer definition
12:40 PM Changeset [851] by mulligan
strong foldl added
12:58 AM Changeset [850] by sacerdot
More informative foldl: foldll.

May 26, 2011:

6:41 PM Changeset [849] by sacerdot
6:26 PM Changeset [848] by sacerdot
2:16 PM Changeset [847] by sacerdot
Several bugs fixed in Matita.

May 25, 2011:

6:10 PM Changeset [846] by mulligan
changes
6:09 PM Changeset [845] by sacerdot
Nightmare…
4:26 PM Changeset [844] by sacerdot
Useless code removed.
3:57 PM Changeset [843] by sacerdot
Function moved from Interpret to Status.
3:57 PM Changeset [842] by sacerdot
Bug fixed.
2:33 PM Changeset [841] by sacerdot
Minor changes.
1:57 PM Changeset [840] by sacerdot
sigma defined
1:31 PM Changeset [839] by sacerdot
More experiments.
12:08 PM Changeset [838] by sacerdot
Restored.
11:49 AM Changeset [837] by mulligan
changes complete
11:43 AM Changeset [836] by mulligan
changes to assembly functions
11:06 AM Changeset [835] by sacerdot
Old experiments removed.
12:10 AM Changeset [834] by sacerdot
Russell at work.

May 24, 2011:

11:19 PM Changeset [833] by sacerdot
Bug fixed to make the file compile. But the type of the assembly …
6:40 PM Changeset [832] by mulligan
work from today
4:01 PM Changeset [831] by sacerdot
Progress in proofs.
2:27 PM Changeset [830] by campbell
Move files that accidentally ended up in the root of the repository.
2:06 PM Changeset [829] by sacerdot
1:32 PM Changeset [828] by sacerdot
Proof statement.
1:26 PM Changeset [827] by sacerdot
The preamble is now part of the PseudoStatus?.

May 23, 2011:

6:39 PM Changeset [826] by mulligan
start of proof
6:12 PM Changeset [825] by mulligan
lots of refactoring, finally got something to prove
5:39 PM Changeset [824] by campbell
Some work on showing that casts around integer operations can be removed.
4:24 PM Changeset [823] by mulligan
added new file for proof of correctness of pseudo-assembly translation
4:22 PM Changeset [822] by mulligan
removed all axioms
3:23 PM Changeset [821] by mulligan
changes to introduce pseudostatus

May 20, 2011:

6:09 PM Changeset [820] by mulligan
changes to get the semantics of pseudoassembly working

May 19, 2011:

4:45 PM Changeset [819] by mulligan
Final changes. Under 8 pages.
4:03 PM Changeset [818] by ayache
32 and 16 bits operations support in D2.2/8051
3:16 PM Changeset [817] by mulligan
final changes, now to get under 8 pages
3:06 PM Changeset [816] by campbell
Clight to Cminor compilation, modulo switch statements, temporary …
12:24 PM Changeset [815] by mulligan
some changes

May 18, 2011:

3:33 PM Changeset [814] by mulligan
changes with claudio

May 16, 2011:

6:07 PM Changeset [813] by mulligan
added boxing of matita code to distinguish from o'caml
5:43 PM Changeset [812] by mulligan
small change
5:35 PM Changeset [811] by mulligan
small typo fixed
5:12 PM Changeset [810] by mulligan
More added.
4:32 PM Changeset [809] by mulligan
more changes to get everything to fit correctly. gone past 8 pg limit
10:44 AM Changeset [808] by mulligan
Changes to paper to get it ready for FMCAD

May 13, 2011:

6:31 PM Changeset [807] by mulligan
small change
6:29 PM Changeset [806] by mulligan
more changes to language used
6:21 PM Changeset [805] by sacerdot
6:18 PM Changeset [804] by sacerdot
6:07 PM Changeset [803] by mulligan
more changes
5:55 PM Changeset [802] by sacerdot
5:50 PM Changeset [801] by mulligan
Changes to english in letter.
5:36 PM Changeset [800] by sacerdot
Half finished.
5:35 PM Changeset [799] by mulligan
more changes.
1:10 PM Changeset [798] by campbell
Fix usual matita tactic mistake.
1:10 PM Changeset [797] by campbell
Add error messages wherever the error monad is used. Sticks to …
1:10 PM Changeset [796] by campbell
Put correct type on cost label expressions in the prototype.
12:29 PM Changeset [795] by mulligan
Changes from this morning.

May 12, 2011:

7:19 PM Changeset [794] by stark
Some content for addendum
5:33 PM Changeset [793] by mulligan
Work from today on rtlabs -> rtl pass.

May 11, 2011:

5:06 PM Changeset [792] by amadio
Deliverable D2.1 with addendum
2:01 PM Changeset [791] by stark
Empty addendum
11:44 AM PublicationVenues edited by mulligan
(diff)

May 10, 2011:

5:50 PM Changeset [790] by campbell
A little tidying: get rid of requirement for jmeq in Mem.ma, remove …
5:36 PM Changeset [789] by mulligan
More work on rtlabs -> rtl pass.

May 9, 2011:

5:52 PM RelatedWork edited by campbell
(diff)
Note: See TracTimeline for information about the timeline view.