Context Navigation

Timeline

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

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

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

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

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

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

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

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

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

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

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

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

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

15:47 Changeset [788] by campbell: Add newer files to experimental Cminor branch.
11:45 Changeset [787] by campbell: Update experimental version of Cminor semantics.

12:48 Changeset [786] by campbell: A version of the clight matita term printer for the current prototype.
11:38 Changeset [785] by sacerdot: Addenda required by the reviewers.

Note: See TracTimeline for information about the timeline view.