

@1770

9 years 
mulligan 
…



@1769

9 years 
sacerdot 
..



@1768

9 years 
sacerdot 
…



@1767

9 years 
mulligan 
…



@1766

9 years 
mulligan 
avoid conflicts



@1765

9 years 
campbell 
Rule out final states in nonterminating executions chunks (RTLabs …



@1764

9 years 
campbell 
Terminating function preserve the property that the execution does not …



@1763

9 years 
mulligan 
to avoid conflicts



@1762

9 years 
sacerdot 
Changes and fixes.



@1761

9 years 
sacerdot 
…



@1760

9 years 
mulligan 
avoiding conflicts



@1759

9 years 
sacerdot 
Tentative agenda.



@1758

9 years 
campbell 
Minor improvements to frontend; add an overall statement.



@1757

9 years 
sacerdot 
…



@1756

9 years 
sacerdot 
Improved outline.



@1755

9 years 
sacerdot 
…



@1754

9 years 
sacerdot 
…



@1753

9 years 
sacerdot 
…



@1752

9 years 
sacerdot 
…



@1751

9 years 
mulligan 
Commit to avoid conflicts with Claudio



@1750

9 years 
tranquil 
start of ERTL to LTL



@1749

9 years 
sacerdot 
Rephrased introduction.



@1748

9 years 
mulligan 
commit to avoid conflicts



@1747

9 years 
boender 
 New and updated version of effort table



@1746

9 years 
campbell 
Revisions to frontend text.



@1745

9 years 
sacerdot 
Conclusions.



@1744

9 years 
boender 
 New version of effort table



@1743

9 years 
mulligan 
diagrams finished, adding text



@1742

9 years 
boender 
 committed new version of effort table



@1741

9 years 
sacerdot 
…



@1740

9 years 
sacerdot 
…



@1739

9 years 
sacerdot 
Footnote for optimizations.



@1738

9 years 
boender 
 small change (layout)



@1737

9 years 
boender 
 small change



@1736

9 years 
campbell 
Show that the bound on the number of instructions until a cost label …



@1735

9 years 
mulligan 
a bit more added



@1734

9 years 
mulligan 
followed brian's lead in explaining the backend translation steps with …



@1733

9 years 
campbell 
More on frontend.



@1732

9 years 
campbell 
More on frontend.



@1731

9 years 
campbell 
A bit of frontend proof outline.



@1730

9 years 
sacerdot 
Minor changes while studying the proof.



@1729

9 years 
sacerdot 
Comment left from SVN merge removed.



@1728

9 years 
mulligan 
avoiding conflicts



@1727

9 years 
boender 
 added last RTL  ERTL diagrams



@1726

9 years 
mulligan 
Finished description of LTL to LIN



@1725

9 years 
mulligan 
commit to avoid conflicts



@1724

9 years 
boender 
 added diagrams to RTL to ERTL section



@1723

9 years 
mulligan 
added more to header of file, commit to avoid conflicts with jaap



@1722

9 years 
mulligan 
changes to english in third part of report



@1721

9 years 
mulligan 
some changes to the report



@1720

9 years 
sacerdot 
New draft.



@1719

9 years 
campbell 
Show that nontermination survives a terminating function call.



@1718

9 years 
mulligan 
added skull.sty for daemon (skull) symbol



@1717

9 years 
mulligan 
added diagrams.sty for drawing commutative diagrams



@1716

9 years 
mulligan 
proof outline, as requested by referees, being typed up in latex



@1715

9 years 
sacerdot 
Some progress.



@1714

9 years 
sacerdot 
…



@1713

9 years 
campbell 
Add a distinguished final state to the frontend languages to match up …



@1712

9 years 
campbell 
Show that constructing an RTLabs structure trace really does use a …



@1711

9 years 
mulligan 
finished block_cost' proof: 1.5 minutes to typecheck qed.



@1710

9 years 
mulligan 
changes from friday afternoon



@1709

9 years 
mulligan 
Changes to the execution of the MOVC instruction



@1708

9 years 
mulligan 
Change to the execution of the MOVC instruction



@1707

9 years 
campbell 
Progress on finite segments of infinite RTLabs structured trace.



@1706

9 years 
campbell 
Checkpoint RTLabs structured traces.



@1705

9 years 
campbell 
Checkpoint RTLabs labelling soundness work.



@1704

9 years 
amadio 
typo



@1703

9 years 
tranquil 
minimal change



@1702

9 years 
tranquil 
updated the report and changed a bit the names



@1701

9 years 
tranquil 
added updated compiler tarball



@1700

9 years 
tranquil 
updated README



@1699

9 years 
amadio 
5.1 up



@1698

9 years 
tranquil 
minor modifications



@1697

9 years 
mulligan 
important bug found



@1696

9 years 
mulligan 
finished adding russell types to the traverse_cost_* functions



@1695

9 years 
mulligan 
Progress on CostsProof?.ma file.



@1694

9 years 
tranquil 
indexed labels branch



@1693

9 years 
mulligan 
Changes to ASMCosts and CostsProofs? files to get everything working again.



@1692

9 years 
mulligan 
resolved conflict in asm costs this morning



@1691

9 years 
sacerdot 
Some progress in the proof: less daemons, less hypotheses in lemmas.



@1690

9 years 
tranquil 
nested loops are not supported yet, the only test had one



@1689

9 years 
tranquil 
kept out the wrapper (which I did not touch, so not sure it works)



@1688

9 years 
amadio 
up d5.15.3



@1687

9 years 
tranquil 
corrected title



@1686

9 years 
tranquil 
corrected abstract



@1685

9 years 
tranquil 
adjusted comparison with aiT



@1684

9 years 
mulligan 
changes from the past week



@1683

9 years 
tranquil 
abstract and running example



@1682

9 years 
campbell 
Complete proof for as_after_return for RTLabs.



@1681

9 years 
campbell 
Checkpoint of stack preservation work in RTLabs.



@1680

9 years 
campbell 
Comment out unused tailcalls in Cminor and RTLabs.
(They would be a …



@1679

9 years 
ayache 
FramaC plugin (sources+documentation)



@1678

9 years 
mulligan 
finished editing the english in the report



@1677

9 years 
mulligan 
changes to paolo's english in the report, about a 1/4 of the way through



@1676

9 years 
tranquil 
corrected some faults
still TODO: running example, language corrections



@1675

9 years 
campbell 
Some work on sound labelled for RTLabs.



@1674

9 years 
tranquil 
corrected some faults
still TODO: running example, language corrections



@1673

9 years 
tranquil 
report on indexed labels
TODO: corrections, examples, etc



@1672

9 years 
campbell 
Matita now generates a couple of inversion lemmas that were manually …



@1671

9 years 
campbell 
A little more on RTLabs infinite traces.


