Timeline



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)

Jun 25, 2011:

2:32 AM Changeset [1043] by sacerdot
Axiom commented out.
2:30 AM Changeset [1042] by sacerdot
Dead code removed. Slow code uncommented.

Jun 24, 2011:

5:05 PM Changeset [1041] by sacerdot
fetch_assembly is still working after bug fix
4:54 PM Changeset [1040] by sacerdot
Bug fixed in assembly.
2:11 PM Changeset [1039] by sacerdot
fetch_assembly_pseudo2 repaired from dependent type madness

Jun 23, 2011:

5:40 PM Changeset [1038] by boender
- some more BVT improvements
2:56 AM Changeset [1037] by sacerdot
Main theorem: comments are working again.

Jun 22, 2011:

11:38 PM Changeset [1036] by sacerdot
11:06 PM Changeset [1035] by sacerdot
Main theorem (broken because of dependent types) almost restored.
5:37 PM WikiStart edited by mulligan
(diff)
5:36 PM WikiStart edited by mulligan
(diff)
5:36 PM WikiStart edited by mulligan
(diff)
5:30 PM WikiStart edited by mulligan
(diff)
5:30 PM WikiStart edited by mulligan
(diff)
5:29 PM WikiStart edited by mulligan
(diff)
5:29 PM WikiStart edited by mulligan
(diff)
5:23 PM WikiStart edited by mulligan
(diff)
4:03 PM Changeset [1034] by boender
various & sundry fold/forall lemmas

Jun 21, 2011:

3:08 PM Changeset [1033] by sacerdot
ispelled & submitted
3:04 PM Changeset [1032] by sacerdot
Final version.
2:25 PM Changeset [1031] by sacerdot
..
2:24 PM Changeset [1030] by sacerdot
2:23 PM Changeset [1029] by sacerdot
2:08 PM Changeset [1028] by sacerdot
One more sentence restored and fitted in.
2:02 PM Changeset [1027] by sacerdot
Bug fixed in figure.
12:47 PM Changeset [1026] by mulligan
final version? under 16 pages
12:35 PM Changeset [1025] by mulligan
removing stray single words to reduce page usage
12:27 PM Changeset [1024] by mulligan
tidied explanation of proof
12:23 PM Changeset [1023] by mulligan
changes to english in matita section, shrunk diagrams in introduction …
12:18 PM Changeset [1022] by sacerdot
12:15 PM Changeset [1021] by mulligan
tidied english in sect 3
12:09 PM Changeset [1020] by sacerdot
More on Matita.
11:39 AM Changeset [1019] by sacerdot
Finished rewriting of Section 3.
11:21 AM Changeset [1018] by mulligan
tidying
11:15 AM Changeset [1017] by mulligan
complete, just under 16 pages
10:20 AM Changeset [1016] by sacerdot
Many fixes to the code snippets.
4:27 AM Changeset [1015] by sacerdot
One intermediate version of main_thm0 close to be repaired.
2:02 AM Changeset [1014] by sacerdot
The main theorem is completely broken (again).
1:52 AM Changeset [1013] by mulligan
more added
12:33 AM Changeset [1012] by mulligan
just a few things left to change

Jun 20, 2011:

6:39 PM Changeset [1011] by mulligan
6:18 PM Changeset [1010] by mulligan
more added, finished up to end of subsect 3.2
6:01 PM Changeset [1009] by mulligan
added line number counts, etc.
5:58 PM Changeset [1008] by mulligan
5:57 PM Changeset [1007] by mulligan
added explanation of sdcc
5:51 PM Changeset [1006] by boender
- added fold + lemmas on fold
5:41 PM Changeset [1005] by sacerdot
5:32 PM Changeset [1004] by mulligan
changes to typesetting
5:30 PM Changeset [1003] by sacerdot
5:27 PM Changeset [1002] by sacerdot
5:26 PM Changeset [1001] by mulligan
reworded intro
5:25 PM Changeset [1000] by sacerdot
5:07 PM Changeset [999] by mulligan
conclusions
5:05 PM Changeset [998] by sacerdot
Half repaired, half broken. Most functions no longer return option …
3:43 PM Changeset [997] by mulligan
minor linguistic polishing
3:41 PM Changeset [996] by sacerdot
Minor fixes.
3:27 PM Changeset [995] by mulligan
changes
Note: See TracTimeline for information about the timeline view.