Timeline



Jul 27, 2011:

5:56 PM Changeset [1090] by mulligan
small change to liveness analysis
5:50 PM Changeset [1089] by mulligan
more changes from earlier in the week
5:50 PM Changeset [1088] by mulligan
work on liveness analysis: an imperative nightmare

Jul 25, 2011:

2:58 PM Changeset [1087] by campbell
Experimental branch where lookups of local variables in Cminor code …
12:41 PM Changeset [1086] by campbell
Branch for experimenting with identifier binding guarantees.

Jul 21, 2011:

5:09 PM Changeset [1085] by mulligan
removed stray files that are no longer needed
5:00 PM Changeset [1084] by mulligan
more added on ertl pass: not sure how much should be axiomatised wrt …
12:28 PM Changeset [1083] by mulligan
ertl --> ltl statement generation nearly complete. required some …

Jul 20, 2011:

5:17 PM Changeset [1082] by mulligan
work from today on ertl -> ltl pass
11:26 AM Changeset [1081] by mulligan
completed rtl-ertl pass

Jul 19, 2011:

5:28 PM Changeset [1080] by mulligan
more added
4:30 PM Changeset [1079] by mulligan
finished rtl to ertl pass modulo conversion of tailcall simplification code
12:39 PM Changeset [1078] by campbell
Implement stack allocation for parameters whose address is taken.
12:23 PM Changeset [1077] by mulligan
ack, dependent types are scary

Jul 18, 2011:

5:40 PM Changeset [1076] by mulligan
small changes
5:21 PM Changeset [1075] by mulligan
nearly completed rtl -> ertl pass removing all option types with dep. types
12:44 PM Changeset [1074] by boender
- added lookup lemma

Jul 15, 2011:

5:38 PM Changeset [1073] by mulligan
more changes from today
4:56 PM Changeset [1072] by campbell
Use not equals form of showing entry/exit labels.
2:40 PM Changeset [1071] by mulligan
changes the specific form that the added proofs take to use None, not …
12:56 PM Changeset [1070] by campbell
Show that entry and exit labels are in the RTLabs graph.
12:56 PM Changeset [1069] by campbell
Change odd proof obligation problem back.

Jul 14, 2011:

2:27 PM Changeset [1068] by mulligan
rtlabs translation complete subject to axioms

Jul 13, 2011:

5:37 PM Changeset [1067] by mulligan
more smaller changes
5:12 PM Changeset [1066] by mulligan
changes from today
4:02 PM Changeset [1065] by campbell
Note a couple of deviations from the prototype.

Jul 12, 2011:

5:52 PM Changeset [1064] by mulligan
changes from today, nearly complete rtlabs translation pass

Jul 11, 2011:

5:52 PM Changeset [1063] by mulligan
changes from today
2:09 PM Changeset [1062] by mulligan
separated jmeq and coercions from foldstuff.ma in order to fix the …

Jul 8, 2011:

5:49 PM Changeset [1061] by mulligan
more work, bug found, ridiculous map3 function with dep. types added
12:17 PM Changeset [1060] by mulligan
work from this morning and yesterday

Jul 6, 2011:

6:09 PM Changeset [1059] by mulligan
work from today, bit of a mess at the moment
1:29 PM Changeset [1058] by campbell
Evict CompCert? Maps interface in favour of BitVectorTries?.

Jul 5, 2011:

5:53 PM Changeset [1057] by mulligan
changes from today
4:25 PM Changeset [1056] by campbell
Switch to delayed identifier error scheme.
12:15 PM Changeset [1055] by mulligan
changes to how identifiers are generated
9:51 AM Changeset [1054] by boender
- proven policy safe

Jul 4, 2011:

6:20 PM Changeset [1053] by mulligan
changes
3:31 PM Changeset [1052] by mulligan
removed offsets after reading cerco mailing list
1:49 PM Changeset [1051] by mulligan
removed superfluous addressing mode code from RTLabs/syntax.ma
10:43 AM Changeset [1050] by mulligan
adding dependent types to map datastructure to remove all option …

Jul 1, 2011:

5:45 PM Changeset [1049] by mulligan
more stuff added
5:11 PM Changeset [1048] by mulligan
added implementation of haskell associative maps to clean up the mess …

Jun 29, 2011:

5:38 PM Changeset [1047] by mulligan
more work from today
12:15 PM Changeset [1046] by mulligan
syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
10:47 AM Changeset [1045] by mulligan
resolved conflict in rtlabs

Jun 27, 2011:

2:17 PM Changeset [1044] by boender
- more fold/forall stuff
12:28 PM AssemblerFormalisation edited by mulligan
(diff)
12:27 PM AssemblerFormalisation edited by mulligan
(diff)
12:27 PM AssemblerFormalisation edited by mulligan
(diff)
12:26 PM AssemblerFormalisation edited by mulligan
(diff)
12:25 PM AssemblerFormalisation edited by mulligan
(diff)
12:24 PM latest.tar.bz2 attached to AssemblerFormalisation by mulligan
Latest bundle of development files.
12:24 PM AssemblerFormalisation created by mulligan
12:05 PM WikiStart edited by mulligan
(diff)
Note: See TracTimeline for information about the timeline view.