Timeline



Oct 29, 2012:

6:19 PM Changeset [2418] by campbell
Add a checking function for the uniqueness of cost labels in RTLabs …

Oct 25, 2012:

4:36 PM Changeset [2417] by boender
- reverted changes to StructuredTraces? (shouldn't have been committed …
12:30 PM Changeset [2416] by mulligan
Some more minor changes

Oct 23, 2012:

3:57 PM Changeset [2415] by campbell
Add the ability to map blocks to symbols in preparation for stack space.
2:43 PM Changeset [2414] by mulligan
Added bib file, done a little bit of rearrangement.
11:15 AM Changeset [2413] by tranquil
* tal_rel corrected to include cases where tal_base_call \approx …

Oct 22, 2012:

4:21 PM Changeset [2412] by campbell
Tidy up measurable definition a bit more.

Oct 20, 2012:

8:08 PM Changeset [2411] by sacerdot
Extensible records implemented via option type. One axiom left.

Oct 19, 2012:

5:05 PM Changeset [2410] by mulligan
Changes to Section 2.
4:48 PM Changeset [2409] by mulligan
Some text about algebraic data types and their limitations. Needs to …
2:07 PM Changeset [2408] by sacerdot
11:18 AM Changeset [2407] by campbell
Sigh, continue in for loops was broken too.

Oct 18, 2012:

6:35 PM Changeset [2406] by sacerdot
Elimination principle committed.
5:29 PM Changeset [2405] by sacerdot
Type of elimination principle generated + more lemmas.
4:10 PM Changeset [2404] by sacerdot
Example finished.
3:57 PM Changeset [2403] by sacerdot
More work, example almost finished up to recursive type.
3:36 PM Changeset [2402] by sacerdot
Progress on parametric types.
1:41 PM Changeset [2401] by mulligan
For Jaap's delight.
1:40 PM Changeset [2400] by sacerdot
Some tests.

Oct 17, 2012:

6:45 PM Changeset [2399] by campbell
Fill in some details about the statement of correctness.
3:35 PM Changeset [2398] by boender
- committed start of stacksize
12:27 PM Changeset [2397] by mulligan
Knocked the initial skeleton into some form of compilable state
12:20 PM Changeset [2396] by mulligan
Polymorphic variants paper skeleton

Oct 12, 2012:

3:33 PM Changeset [2395] by campbell
Proper handling of comparison of pointers off-the-end of an object. We …
12:59 PM Changeset [2394] by campbell
I've kept the odd note on bits of CerCo? work I've been doing. James …

Oct 10, 2012:

5:56 PM Changeset [2393] by campbell
A pointer comparison test case that illustrates a bug.
5:18 PM Changeset [2392] by campbell
Labelling translations of && and || need a lot of cost labelling to …

Oct 9, 2012:

3:10 PM Changeset [2391] by campbell
Revert "Put the post-loop cost label into the Clight while statement …

Oct 5, 2012:

12:57 PM Changeset [2390] by campbell
Tidy up a corner case when generating RTLabs so that we generate less …
12:57 PM Changeset [2389] by campbell
Fix dowhile statements, and carefully arrange the translation so that …
12:57 PM Changeset [2388] by campbell
Example of each type of control flow statement, plus minor fix to …

Oct 3, 2012:

1:27 PM Changeset [2387] by garnier
Revamped memory extensions, proved stuff on freeing blocks and on …
1:26 PM Changeset [2386] by garnier
Implementation of constructive finite sets based on lists. Various …
11:33 AM Changeset [2385] by campbell
Minor housekeeping.

Oct 1, 2012:

6:21 PM Changeset [2384] by campbell
Move Matita pretty printers into place.
5:58 PM Changeset [2383] by campbell
Branch prototype so that there's a version with the matita output …
11:55 AM Changeset [2382] by campbell
Final version of executable semantics paper.
11:55 AM Changeset [2381] by campbell
Executable semantics paper as it was in the first submission.
Note: See TracTimeline for information about the timeline view.