Timeline



Feb 6, 2013:

11:51 PM Changeset [2637] by sacerdot
11:43 PM Changeset [2636] by campbell
Extracted front-end.
11:28 PM Changeset [2635] by sacerdot
11:23 PM Changeset [2634] by sacerdot
11:16 PM Changeset [2633] by sacerdot
11:11 PM Changeset [2632] by sacerdot
10:28 PM Changeset [2631] by sacerdot
10:19 PM Changeset [2630] by sacerdot
10:19 PM Changeset [2629] by sacerdot
10:18 PM Changeset [2628] by sacerdot
10:06 PM Changeset [2627] by sacerdot
9:32 PM Changeset [2626] by sacerdot
8:14 PM Changeset [2625] by sacerdot
6:39 PM Changeset [2624] by campbell
Properly evict unused and axiomatised Floats.
6:39 PM Changeset [2623] by campbell
Name change update.
6:11 PM Changeset [2622] by sacerdot
5:53 PM Changeset [2621] by sacerdot
5:03 PM Changeset [2620] by campbell
Sufficient hacking to run the extracted Clight semantics.
5:03 PM Changeset [2619] by campbell
Update some test cases.
5:03 PM Changeset [2618] by campbell
Tidy up measurable a little.
5:03 PM Changeset [2617] by campbell
Trivial simplification on split_trace.
4:07 PM Changeset [2616] by sacerdot
3:51 PM Changeset [2615] by sacerdot
3:39 PM Changeset [2614] by sacerdot
3:30 PM Changeset [2613] by sacerdot
3:15 PM Changeset [2612] by sacerdot
2:21 PM Changeset [2611] by sacerdot
2:00 PM Changeset [2610] by sacerdot
1:56 PM Changeset [2609] by sacerdot
Bibliography in place.
1:01 PM Changeset [2608] by garnier
Regions are no more stored in blocks. block_region now tests the id, …
12:15 PM Changeset [2607] by sacerdot
authors fixed
12:13 PM Changeset [2606] by sacerdot
conclusions
10:30 AM Changeset [2605] by sacerdot
A tentative submission to itp-2013. We will probably not submit the …

Feb 5, 2013:

10:49 PM Changeset [2604] by piccolo
ERTLtoERTLptr in place.
1:54 PM Changeset [2603] by piccolo
Dead code commented out.
1:54 PM Changeset [2602] by piccolo
Dead code commented out.
1:36 PM Changeset [2601] by sacerdot
Extraction to ocaml is now working, with a couple of bugs left. One …

Feb 1, 2013:

12:13 PM Changeset [2600] by garnier
Memory injections are now only defined relatively to block ids, not …

Jan 31, 2013:

5:15 PM Changeset [2599] by tranquil
* map_opt and map on positive maps are now clean (erase empty …
12:56 PM Changeset [2598] by garnier
Tentative, partial draft for the definition of Clight-Cminor …
12:07 PM Changeset [2597] by campbell
Some work in progress on measurable subtrace preservation.
12:06 PM Changeset [2596] by campbell
Use a simpler stack cost map, and then specialise to each semantics.

Jan 30, 2013:

7:25 PM Changeset [2595] by tranquil
* dropped locals and exit from definition of joint_if_function * new …

Jan 29, 2013:

8:28 PM Changeset [2594] by garnier
Some fixes in memory injections, and some holes filled.
12:13 PM Changeset [2593] by mckinna
Finally chased down wicked failure to close case 1.1: of …
11:20 AM Changeset [2592] by piccolo
main lemma of ERTLptr in place

Jan 28, 2013:

11:43 AM Changeset [2591] by garnier
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …

Jan 24, 2013:

7:52 PM Changeset [2590] by piccolo
added monad machineary for ERTL to ERTLptr translation eval_seq_no_pc …

Jan 23, 2013:

4:34 PM Changeset [2589] by campbell
Add one of the simulation diagrams
2:38 PM Changeset [2588] by garnier
modified Cexec/Csem? semantics: . force andbool and orbool types to be …
1:51 PM Changeset [2587] by campbell
Tweak talk a little.
1:19 PM Changeset [2586] by amadio
r
12:26 PM Changeset [2585] by campbell
Many improvements to proof/structured traces talk.
5:58 AM Changeset [2584] by regisgia
* Update slides.

Jan 21, 2013:

10:58 PM Changeset [2583] by campbell
Structured traces talk with most of the content; not quite final.
11:22 AM HiPEAC13 edited by campbell
(diff)
11:22 AM HiPEAC13 edited by campbell
(diff)

Jan 15, 2013:

3:58 PM Changeset [2582] by garnier
Some progress on CL to CM.
3:45 PM Changeset [2581] by mckinna
commented out back end entirely until knock-on effects of changes to …
3:42 PM Changeset [2580] by campbell
Note on ptr + int vs int + ptr.
11:21 AM HiPEAC13 edited by campbell
(diff)

Jan 14, 2013:

1:37 PM Changeset [2579] by regisgia
* First version of Yann's slides.

Jan 11, 2013:

9:36 PM Changeset [2578] by garnier
Progress on CL to CM, fixed some stuff in memory injections.
5:05 PM HiPEAC13 edited by sacerdot
(diff)
5:03 PM logo-hipeac.png attached to HiPEAC13 by sacerdot
HiPEAC logo
5:02 PM HiPEAC13 edited by sacerdot
(diff)
5:00 PM Changeset [2577] by tranquil
abstract of indexed labels talk
4:09 PM WikiStart edited by campbell
(diff)
4:09 PM WikiStart edited by campbell
(diff)
4:08 PM WikiStart edited by campbell
(diff)

Jan 10, 2013:

3:57 PM Changeset [2576] by campbell
Add conditional test case that also uses switch removal.

Jan 9, 2013:

8:51 PM Changeset [2575] by mckinna
temporary commit localised the source of trouble in the proof of …
6:33 PM Changeset [2574] by campbell
Update labelling simulation proofs due to some changes elsewhere.
6:15 PM Changeset [2573] by mckinna
temporary fixes to ensure {compiler,correctness}.ma recompile after …
1:23 PM Changeset [2572] by garnier
Progress on toCminorCorrectness.

Jan 8, 2013:

5:46 PM Changeset [2571] by campbell
Lots of little changes for cl_tailcall and classifier change.
Note: See TracTimeline for information about the timeline view.