Timeline



Nov 6, 2012:

5:00 PM Changeset [2437] by tranquil
generalised calls to calls with pointers
4:13 PM Changeset [2436] by tranquil
small changes
4:12 PM Changeset [2435] by tranquil
new back end operations
4:04 PM Changeset [2434] by campbell
Misc notes.
4:02 PM Changeset [2433] by campbell
Tidy up Clight pointer comparison.
3:17 PM Changeset [2432] by campbell
Remove off-the-end pointers from front end ops.
1:15 PM Changeset [2431] by campbell
Fix in matita-out branch too.
1:13 PM Changeset [2430] by campbell
Fix casting for conditionals in CompCert?-derived C parser.
12:53 PM Changeset [2429] by garnier
Restrict semantics of pointer comparison to what CompCert? does - i.e. …
12:02 PM Changeset [2428] by campbell
Tighten requirements on switch statements in Clight to only give …

Nov 5, 2012:

11:14 AM Changeset [2427] by mulligan
More work on explanation.

Oct 31, 2012:

5:36 PM Changeset [2426] by boender
- updated stacksize to reflect new developments, completed proof - …
3:33 PM Changeset [2425] by mulligan
Garrigue's stuff completely added to the paper. Need to explain the …
12:59 PM Changeset [2424] by mulligan
Changes to the file including making a start on incorporating …

Oct 30, 2012:

5:23 PM Changeset [2423] by tranquil
as_classifier predicate → as_classify function as_call predicate from …
4:23 PM Changeset [2422] by tranquil
adapted joint to cl_call f
4:18 PM Changeset [2421] by tranquil
added simulation of flat prefix, and comments to explain the code
12:32 PM Changeset [2420] by campbell
Tidy away generic results about folds on positive/identifier maps.
11:52 AM Changeset [2419] by mulligan
Some initial work.

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 …
Note: See TracTimeline for information about the timeline view.