

@1902

10 years 
mulligan 
Reverted needless changes to StructuredTraces?



@1901

10 years 
mulligan 
Slight changes to StructuredTraces?: should not change too much



@1900

10 years 
mulligan 
CostProof? complete, modulo some daemons and axioms in earlier files



@1899

10 years 
mulligan 
Changes to statements of theorems



@1898

10 years 
mulligan 
Ported changes from ASMCosts.ma into CostsProof?.ma and got everything …



@1897

10 years 
mulligan 
Changes to proof, and pushed through those changes to rest of the file.



@1896

10 years 
mulligan 
Finished horror proof



@1895

10 years 
mulligan 
Split the ASMCosts files while working on traverse_code_internal. A …



@1894

10 years 
mulligan 
Closed a hole in the proof by deriving a contradiction using even_p …



@1893

10 years 
campbell 
Show stronger result about labelling of expressions.



@1892

10 years 
mulligan 
Lots of work from today



@1891

10 years 
mulligan 
Nightmarish proofs on bitvectors. Trying to find some way of making …



@1890

10 years 
boender 
 added comment about bitvector translation



@1889

10 years 
boender 
 some pages of article



@1888

10 years 
campbell 
Show that labelling of expressions works ...
after fixing it to match …



@1887

10 years 
boender 
 added SEFM2012 directory
 some progress in assembly



@1886

10 years 
boender 
 improvements for disambiguation and quick(er) typing



@1885

10 years 
boender 
 updated assembler with new definition of occurs_exactly_once



@1884

10 years 
campbell 
Syntax changes to fit Paolo's commit.



@1883

10 years 
campbell 
Ilias' switch removal code, plus a test.



@1882

10 years 
tranquil 
big update, alas incomplete:
joint changed a bit, and all BE languages …



@1881

10 years 
campbell 
Resurrect version of exec_up_to which shows the final state.



@1880

10 years 
campbell 
Show that RTLabs flat traces are determined by their starting state, …



@1879

10 years 
boender 
 Policy compiles until the end, still some (fairly trivial) cases …



@1878

10 years 
campbell 
Enforce typing of constants in frontend, plus binops for RTLabs.



@1877

10 years 
campbell 
Update RTLabs structured traces for typed binops and new memory model.



@1876

10 years 
campbell 
Update Cexec soundness proof.
Change finishes_with predicate to …



@1875

10 years 
campbell 
Update brief memory model test.



@1874

10 years 
campbell 
First cut at using backend memory model throughout.
Note the …



@1873

10 years 
campbell 
Fix up earlier frontend value conversion work.



@1872

10 years 
campbell 
Make binary operations in Cminor/RTLabs properly typed.
A few extra …



@1871

10 years 
campbell 
Change Clight to Cminor compilation to use gotos rather than loops, …



@1870

10 years 
boender 
 changed sigma00 in Assembly to use foldl_strong + proved invariants …



@1869

10 years 
mulligan 
a load of axioms closed in ASMCosts file



@1868

10 years 
Ian Stark 
Put beamer code in the template to remove fungus



@1867

10 years 
mulligan 
Large changes following comments by IS, JMc and CSC



@1866

10 years 
campbell 
Drop "extra detail" from WP3.



@1865

10 years 
tranquil 
my presentation



@1864

10 years 
campbell 
Add PDF for WP3.



@1863

10 years 
campbell 
Minor WP3 revisions.



@1862

10 years 
mulligan 
Changes to presentation



@1861

10 years 
mulligan 
Changes to CSC's changes



@1860

10 years 
sacerdot 
…



@1859

10 years 
mulligan 
Added a new slide with the dynamic cost computation on it



@1858

10 years 
campbell 
Minor WP3 tweak.



@1857

10 years 
sacerdot 
…



@1856

10 years 
mulligan 
Added affiliation to title page



@1855

10 years 
mulligan 
Dynamic cost diagram added



@1854

10 years 
sacerdot 
…



@1853

10 years 
mulligan 
Changed names of labels etc. in diagram



@1852

10 years 
campbell 
Revise WP3 down.



@1851

10 years 
regisgia 
* Slides YRG.



@1850

10 years 
sacerdot 
…



@1849

10 years 
mulligan 
Added title pages to split talk into three separate sections



@1848

10 years 
sacerdot 
…



@1847

10 years 
mulligan 
More changes to presentation based on comments



@1846

10 years 
ayache 
Review 2012: Nicolas's presentation.



@1845

10 years 
campbell 
Minor WP3 revisions prior to more major stuff.



@1844

10 years 
mulligan 
Changed from serif to sans serif fonts



@1843

10 years 
mulligan 
Added svg file for my image for editing in inkscape



@1842

10 years 
mulligan 
Small change to contents frame



@1841

10 years 
mulligan 
Added explicit PDF to directory for printing



@1840

10 years 
mulligan 
Changes to my presentation based on feedback from practice session …



@1839

10 years 
sacerdot 
…



@1838

10 years 
sacerdot 
First version.



@1837

10 years 
boender 
 added first draft of WP6 presentation



@1836

10 years 
campbell 
Revise WP3 presentation.



@1835

10 years 
tranquil 
fixed broken file



@1834

10 years 
tranquil 
presentation: TODO running example and a frame of intro



@1833

10 years 
tranquil 
cleaning up



@1832

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



@1831

10 years 
mulligan 
small changes to asmcosts file to refactor proof



@1830

10 years 
campbell 
Rest of WP3 presentation.



@1829

10 years 
mulligan 
changes to my presentation, just one point left to consider



@1828

10 years 
sacerdot 
…



@1827

10 years 
sacerdot 
Added again.



@1826

10 years 
sacerdot 
Removed because caused problems to the SVN.



@1825

10 years 
campbell 
WP3 draft slides.
Fix fetopen.png.



@1824

10 years 
mulligan 
More changes to presentation, following Claudio's comments



@1823

10 years 
ayache 
Review 2012: Nicolas's presentation.



@1822

10 years 
mulligan 
Finished presentation, added proper CerCo? style.



@1821

10 years 
mulligan 
discussed merges into o'caml compiler. talk complete subject to …



@1820

10 years 
sacerdot 
…



@1819

10 years 
sacerdot 
…



@1818

10 years 
sacerdot 
Moved from D1.1 to D1.2 where it should be.



@1817

10 years 
sacerdot 
Presentations for the second review.



@1816

10 years 
mulligan 
more slides added, only got topic of changes merged back into o'caml …



@1815

10 years 
mulligan 
Added more to talk



@1814

10 years 
mulligan 
renamed file to avoid confusion



@1813

10 years 
mulligan 
Added presentation that I have been working on for Paris meeting next week.



@1812

10 years 
campbell 
Provide a combined type for terminating and nonterminating structured …



@1811

10 years 
boender 
 corrected definition of geb



@1810

10 years 
boender 
 new version of policy that compiles up to the final glue



@1809

10 years 
boender 
 committed partially compiling version of policy (up until …



@1808

10 years 
campbell 
Create a Prop version of the nonterminating structured traces so that …



@1807

10 years 
mulligan 
some changes, as finally worked out what i was up to prior to working …



@1806

10 years 
campbell 
Show that we could construct RTLabs nonterminating structured traces …



@1805

10 years 
campbell 
RTLabs structured traces: package up some of the properties we need …



@1804

10 years 
sacerdot 
The submitted version.



@1803

10 years 
tranquil 
yet another small correction in the LTL to LIN part


