Timeline



Mar 9, 2012:

1:19 PM Changeset [1815] by mulligan
Added more to talk
10:58 AM Changeset [1814] by mulligan
renamed file to avoid confusion
10:54 AM Changeset [1813] by mulligan
Added presentation that I have been working on for Paris meeting next week.

Mar 8, 2012:

12:13 PM Changeset [1812] by campbell
Provide a combined type for terminating and non-terminating structured …
11:37 AM Changeset [1811] by boender
- corrected definition of geb

Mar 7, 2012:

7:16 PM Changeset [1810] by boender
- new version of policy that compiles up to the final glue
1:27 PM Changeset [1809] by boender
- committed partially compiling version of policy (up until …

Mar 6, 2012:

6:06 PM Changeset [1808] by campbell
Create a Prop version of the non-terminating structured traces so that …

Mar 5, 2012:

12:40 PM Changeset [1807] by mulligan
some changes, as finally worked out what i was up to prior to working …
12:38 PM Changeset [1806] by campbell
Show that we could construct RTLabs non-terminating structured traces …
12:38 PM Changeset [1805] by campbell
RTLabs structured traces: package up some of the properties we need …

Mar 2, 2012:

4:28 PM Changeset [1804] by sacerdot
The submitted version.
4:27 PM Changeset [1803] by tranquil
yet another small correction in the LTL to LIN part
3:55 PM Changeset [1802] by tranquil
other small corrections
3:16 PM Changeset [1801] by tranquil
small correction

Mar 1, 2012:

5:29 PM Changeset [1800] by sacerdot
Applied suggestions by Roberto.
4:49 PM Changeset [1799] by sacerdot
Applied Roberto's suggestions.
4:23 PM Changeset [1798] by sacerdot
Applied comments by Brian, Randy and Roberto.

Feb 29, 2012:

2:03 PM Changeset [1797] by mulligan
implemented brian's changes
11:49 AM Changeset [1796] by campbell
Cast removal is also an endo-transformation.

Feb 28, 2012:

6:11 PM Changeset [1795] by sacerdot
Final version, waiting for comments.
6:07 PM Changeset [1794] by mulligan
Added cpp paper as an addendum to the report
5:57 PM Changeset [1793] by sacerdot
5:56 PM Changeset [1792] by mulligan
5:01 PM Changeset [1791] by mulligan
cleaning up
4:35 PM Changeset [1790] by mulligan
edited the report so that all the spelling is consistent (british …
4:25 PM Changeset [1789] by sacerdot
11:32 AM Changeset [1788] by tranquil
small modifications
10:57 AM Changeset [1787] by sacerdot
New proposal.

Feb 27, 2012:

6:40 PM Changeset [1786] by sacerdot
5:55 PM Changeset [1785] by tranquil
finished ERTL to LTL sketch
5:55 PM Changeset [1784] by campbell
Start on proof of existence of nonterminating RTLabs structured traces.
5:55 PM Changeset [1783] by campbell
Remove junk from non-terminating structured traces.
5:55 PM Changeset [1782] by campbell
Correct bad inversion.
5:55 PM Changeset [1781] by mulligan
Reinstated the lstlisting style
5:45 PM Changeset [1780] by mulligan
finished rtl to ertl
5:11 PM Changeset [1779] by mulligan
5:09 PM Changeset [1778] by sacerdot
5:01 PM Changeset [1777] by mulligan
4:53 PM Changeset [1776] by sacerdot
4:11 PM Changeset [1775] by sacerdot
4:08 PM Changeset [1774] by sacerdot
3:53 PM Changeset [1773] by sacerdot
3:46 PM Changeset [1772] by mulligan
3:44 PM Changeset [1771] by mulligan
some typos fixed, commit mostly to avoid conflicts
2:57 PM Changeset [1770] by mulligan
2:52 PM Changeset [1769] by sacerdot
..
2:46 PM Changeset [1768] by sacerdot
2:45 PM Changeset [1767] by mulligan
2:19 PM Changeset [1766] by mulligan
avoid conflicts
2:16 PM Changeset [1765] by campbell
Rule out final states in non-terminating executions chunks (RTLabs …
2:16 PM Changeset [1764] by campbell
Terminating function preserve the property that the execution does not …
1:52 PM Changeset [1763] by mulligan
to avoid conflicts
1:51 PM Changeset [1762] by sacerdot
Changes and fixes.
11:31 AM Changeset [1761] by sacerdot
11:01 AM Changeset [1760] by mulligan
avoiding conflicts
10:02 AM Changeset [1759] by sacerdot
Tentative agenda.

Feb 24, 2012:

7:01 PM Changeset [1758] by campbell
Minor improvements to front-end; add an overall statement.
6:13 PM Changeset [1757] by sacerdot
5:59 PM Changeset [1756] by sacerdot
Improved outline.
5:49 PM Changeset [1755] by sacerdot
5:46 PM Changeset [1754] by sacerdot
5:36 PM Changeset [1753] by sacerdot
5:18 PM Changeset [1752] by sacerdot
5:09 PM Changeset [1751] by mulligan
Commit to avoid conflicts with Claudio
5:02 PM Changeset [1750] by tranquil
start of ERTL to LTL
4:55 PM Changeset [1749] by sacerdot
Rephrased introduction.
4:53 PM Changeset [1748] by mulligan
commit to avoid conflicts
4:25 PM Changeset [1747] by boender
- New and updated version of effort table
4:09 PM Changeset [1746] by campbell
Revisions to front-end text.
4:07 PM Changeset [1745] by sacerdot
Conclusions.
4:03 PM Changeset [1744] by boender
- New version of effort table
3:45 PM Changeset [1743] by mulligan
diagrams finished, adding text
3:40 PM Changeset [1742] by boender
- committed new version of effort table
3:24 PM Changeset [1741] by sacerdot
2:32 PM Changeset [1740] by sacerdot
2:30 PM Changeset [1739] by sacerdot
Footnote for optimizations.
2:05 PM Changeset [1738] by boender
- small change (layout)
2:04 PM Changeset [1737] by boender
- small change
1:19 PM Changeset [1736] by campbell
Show that the bound on the number of instructions until a cost label …
1:00 PM Changeset [1735] by mulligan
a bit more added
11:44 AM Changeset [1734] by mulligan
followed brian's lead in explaining the backend translation steps with …
10:10 AM Changeset [1733] by campbell
More on front-end.

Feb 23, 2012:

7:07 PM Changeset [1732] by campbell
More on front-end.
5:25 PM Changeset [1731] by campbell
A bit of front-end proof outline.
5:17 PM Changeset [1730] by sacerdot
Minor changes while studying the proof.
2:29 PM Changeset [1729] by sacerdot
Comment left from SVN merge removed.
1:48 PM Changeset [1728] by mulligan
avoiding conflicts
1:47 PM Changeset [1727] by boender
- added last RTL - ERTL diagrams
1:14 PM Changeset [1726] by mulligan
Finished description of LTL to LIN
12:51 PM Changeset [1725] by mulligan
commit to avoid conflicts
12:51 PM Changeset [1724] by boender
- added diagrams to RTL to ERTL section
10:41 AM Changeset [1723] by mulligan
added more to header of file, commit to avoid conflicts with jaap

Feb 22, 2012:

5:12 PM Changeset [1722] by mulligan
changes to english in third part of report
2:38 PM Changeset [1721] by mulligan
some changes to the report
2:37 PM Changeset [1720] by sacerdot
New draft.
2:06 PM Changeset [1719] by campbell
Show that non-termination survives a terminating function call.
1:54 PM Changeset [1718] by mulligan
added skull.sty for daemon (skull) symbol
11:28 AM Changeset [1717] by mulligan
added diagrams.sty for drawing commutative diagrams
11:00 AM Changeset [1716] by mulligan
proof outline, as requested by referees, being typed up in latex
10:10 AM Changeset [1715] by sacerdot
Some progress.

Feb 21, 2012:

4:22 PM Changeset [1714] by sacerdot
11:58 AM Changeset [1713] by campbell
Add a distinguished final state to the front-end languages to match up …
11:58 AM Changeset [1712] by campbell
Show that constructing an RTLabs structure trace really does use a …

Feb 20, 2012:

11:15 AM Changeset [1711] by mulligan
finished block_cost' proof: 1.5 minutes to typecheck qed.
10:04 AM Changeset [1710] by mulligan
changes from friday afternoon

Feb 17, 2012:

11:52 AM Changeset [1709] by mulligan
Changes to the execution of the MOVC instruction
11:51 AM Changeset [1708] by mulligan
Change to the execution of the MOVC instruction

Feb 16, 2012:

6:05 PM Changeset [1707] by campbell
Progress on finite segments of infinite RTLabs structured trace.
6:05 PM Changeset [1706] by campbell
Checkpoint RTLabs structured traces.
6:05 PM Changeset [1705] by campbell
Checkpoint RTLabs labelling soundness work.
5:15 PM D5.1-5.3.pdf attached to WikiStart by mulligan
Report for D5.1-5.3
4:54 PM Changeset [1704] by amadio
typo
11:55 AM src20111020.tgz attached to WikiStart by mulligan
Matita snapshot for typechecking recent deliverables
11:54 AM D3-3.pdf attached to WikiStart by mulligan
Deliverable for D3.3
11:54 AM D3-2.pdf attached to WikiStart by mulligan
Deliverable for D3.2
11:48 AM D5.1-5.3.tar.gz attached to WikiStart by mulligan
Deliverable for D5.1-5.3
11:41 AM WikiStart edited by mulligan
change of title for wilmer (diff)
11:36 AM Changeset [1703] by tranquil
minimal change
11:35 AM Changeset [1702] by tranquil
updated the report and changed a bit the names
11:25 AM Changeset [1701] by tranquil
added updated compiler tarball
11:23 AM Changeset [1700] by tranquil
updated README
11:22 AM Changeset [1699] by amadio
5.1 up
11:05 AM Changeset [1698] by tranquil
minor modifications

Feb 15, 2012:

6:02 PM Changeset [1697] by mulligan
important bug found
4:09 PM Changeset [1696] by mulligan
finished adding russell types to the traverse_cost_* functions
2:10 PM Changeset [1695] by mulligan
Progress on CostsProof?.ma file.
9:30 AM Changeset [1694] by tranquil
indexed labels branch

Feb 14, 2012:

4:38 PM Changeset [1693] by mulligan
Changes to ASMCosts and CostsProofs? files to get everything working again.
1:18 PM Changeset [1692] by mulligan
resolved conflict in asm costs this morning
1:43 AM Changeset [1691] by sacerdot
Some progress in the proof: less daemons, less hypotheses in lemmas.

Feb 13, 2012:

3:58 PM Changeset [1690] by tranquil
nested loops are not supported yet, the only test had one
3:54 PM Changeset [1689] by tranquil
kept out the wrapper (which I did not touch, so not sure it works)
9:08 AM Changeset [1688] by amadio
up d5.1-5.3

Feb 10, 2012:

2:12 PM Changeset [1687] by tranquil
corrected title
Note: See TracTimeline for information about the timeline view.