|
|
@1910
|
9 years |
mulligan |
Finished proof modulo termination argument
|
|
|
@1909
|
9 years |
mulligan |
Ported new statements to remainder of Interpret.ma file.
|
|
|
@1908
|
9 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
@1907
|
9 years |
mulligan |
Fixes to get file to compile
|
|
|
@1906
|
9 years |
mulligan |
Statements simplified in block_cost and dependencies
|
|
|
@1905
|
9 years |
boender |
- plugging gap in assembly proof
|
|
|
@1904
|
9 years |
mulligan |
Problem with proof fixed by noting that problem is actually irrelevant
|
|
|
@1903
|
9 years |
mulligan |
Small changes prior to experiment
|
|
|
@1902
|
9 years |
mulligan |
Reverted needless changes to StructuredTraces?
|
|
|
@1901
|
9 years |
mulligan |
Slight changes to StructuredTraces?: should not change too much
|
|
|
@1900
|
9 years |
mulligan |
CostProof? complete, modulo some daemons and axioms in earlier files
|
|
|
@1899
|
9 years |
mulligan |
Changes to statements of theorems
|
|
|
@1898
|
9 years |
mulligan |
Ported changes from ASMCosts.ma into CostsProof?.ma and got everything …
|
|
|
@1897
|
9 years |
mulligan |
Changes to proof, and pushed through those changes to rest of the file.
|
|
|
@1896
|
9 years |
mulligan |
Finished horror proof
|
|
|
@1895
|
9 years |
mulligan |
Split the ASMCosts files while working on traverse_code_internal. A …
|
|
|
@1894
|
9 years |
mulligan |
Closed a hole in the proof by deriving a contradiction using even_p …
|
|
|
@1893
|
9 years |
campbell |
Show stronger result about labelling of expressions.
|
|
|
@1892
|
9 years |
mulligan |
Lots of work from today
|
|
|
@1891
|
9 years |
mulligan |
Nightmarish proofs on bitvectors. Trying to find some way of making …
|
|
|
@1890
|
9 years |
boender |
- added comment about bitvector translation
|
|
|
@1889
|
9 years |
boender |
- some pages of article
|
|
|
@1888
|
9 years |
campbell |
Show that labelling of expressions works ...
after fixing it to match …
|
|
|
@1887
|
9 years |
boender |
- added SEFM2012 directory
- some progress in assembly
|
|
|
@1886
|
9 years |
boender |
- improvements for disambiguation and quick(er) typing
|
|
|
@1885
|
9 years |
boender |
- updated assembler with new definition of occurs_exactly_once
|
|
|
@1884
|
9 years |
campbell |
Syntax changes to fit Paolo's commit.
|
|
|
@1883
|
9 years |
campbell |
Ilias' switch removal code, plus a test.
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
@1881
|
9 years |
campbell |
Resurrect version of exec_up_to which shows the final state.
|
|
|
@1880
|
9 years |
campbell |
Show that RTLabs flat traces are determined by their starting state, …
|
|
|
@1879
|
9 years |
boender |
- Policy compiles until the end, still some (fairly trivial) cases …
|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
@1877
|
9 years |
campbell |
Update RTLabs structured traces for typed binops and new memory model.
|
|
|
@1876
|
9 years |
campbell |
Update Cexec soundness proof.
Change finishes_with predicate to …
|
|
|
@1875
|
9 years |
campbell |
Update brief memory model test.
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
@1873
|
9 years |
campbell |
Fix up earlier front-end value conversion work.
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
@1871
|
9 years |
campbell |
Change Clight to Cminor compilation to use gotos rather than loops, …
|
|
|
@1870
|
9 years |
boender |
- changed sigma00 in Assembly to use foldl_strong + proved invariants …
|
|
|
@1869
|
9 years |
mulligan |
a load of axioms closed in ASMCosts file
|
|
|
@1868
|
9 years |
Ian Stark |
Put beamer code in the template to remove fungus
|
|
|
@1867
|
9 years |
mulligan |
Large changes following comments by IS, JMc and CSC
|
|
|
@1866
|
9 years |
campbell |
Drop "extra detail" from WP3.
|
|
|
@1865
|
9 years |
tranquil |
my presentation
|
|
|
@1864
|
9 years |
campbell |
Add PDF for WP3.
|
|
|
@1863
|
9 years |
campbell |
Minor WP3 revisions.
|
|
|
@1862
|
9 years |
mulligan |
Changes to presentation
|
|
|
@1861
|
9 years |
mulligan |
Changes to CSC's changes
|
|
|
@1860
|
9 years |
sacerdot |
…
|
|
|
@1859
|
9 years |
mulligan |
Added a new slide with the dynamic cost computation on it
|
|
|
@1858
|
9 years |
campbell |
Minor WP3 tweak.
|
|
|
@1857
|
9 years |
sacerdot |
…
|
|
|
@1856
|
9 years |
mulligan |
Added affiliation to title page
|
|
|
@1855
|
9 years |
mulligan |
Dynamic cost diagram added
|
|
|
@1854
|
9 years |
sacerdot |
…
|
|
|
@1853
|
9 years |
mulligan |
Changed names of labels etc. in diagram
|
|
|
@1852
|
9 years |
campbell |
Revise WP3 down.
|
|
|
@1851
|
9 years |
regisgia |
* Slides YRG.
|
|
|
@1850
|
9 years |
sacerdot |
…
|
|
|
@1849
|
9 years |
mulligan |
Added title pages to split talk into three separate sections
|
|
|
@1848
|
9 years |
sacerdot |
…
|
|
|
@1847
|
9 years |
mulligan |
More changes to presentation based on comments
|
|
|
@1846
|
9 years |
ayache |
Review 2012: Nicolas's presentation.
|
|
|
@1845
|
9 years |
campbell |
Minor WP3 revisions prior to more major stuff.
|
|
|
@1844
|
9 years |
mulligan |
Changed from serif to sans serif fonts
|
|
|
@1843
|
9 years |
mulligan |
Added svg file for my image for editing in inkscape
|
|
|
@1842
|
9 years |
mulligan |
Small change to contents frame
|
|
|
@1841
|
9 years |
mulligan |
Added explicit PDF to directory for printing
|
|
|
@1840
|
9 years |
mulligan |
Changes to my presentation based on feedback from practice session …
|
|
|
@1839
|
9 years |
sacerdot |
…
|
|
|
@1838
|
9 years |
sacerdot |
First version.
|
|
|
@1837
|
9 years |
boender |
- added first draft of WP6 presentation
|
|
|
@1836
|
9 years |
campbell |
Revise WP3 presentation.
|
|
|
@1835
|
9 years |
tranquil |
fixed broken file
|
|
|
@1834
|
9 years |
tranquil |
presentation: TODO running example and a frame of intro
|
|
|
@1833
|
9 years |
tranquil |
cleaning up
|
|
|
@1832
|
9 years |
tranquil |
nested loops are not supported yet, the only test had one
|
|
|
@1831
|
9 years |
mulligan |
small changes to asmcosts file to refactor proof
|
|
|
@1830
|
9 years |
campbell |
Rest of WP3 presentation.
|
|
|
@1829
|
9 years |
mulligan |
changes to my presentation, just one point left to consider
|
|
|
@1828
|
9 years |
sacerdot |
…
|
|
|
@1827
|
9 years |
sacerdot |
Added again.
|
|
|
@1826
|
9 years |
sacerdot |
Removed because caused problems to the SVN.
|
|
|
@1825
|
9 years |
campbell |
WP3 draft slides.
Fix fetopen.png.
|
|
|
@1824
|
9 years |
mulligan |
More changes to presentation, following Claudio's comments
|
|
|
@1823
|
9 years |
ayache |
Review 2012: Nicolas's presentation.
|
|
|
@1822
|
9 years |
mulligan |
Finished presentation, added proper CerCo? style.
|
|
|
@1821
|
9 years |
mulligan |
discussed merges into o'caml compiler. talk complete subject to …
|
|
|
@1820
|
9 years |
sacerdot |
…
|
|
|
@1819
|
9 years |
sacerdot |
…
|
|
|
@1818
|
9 years |
sacerdot |
Moved from D1.1 to D1.2 where it should be.
|
|
|
@1817
|
9 years |
sacerdot |
Presentations for the second review.
|
|
|
@1816
|
9 years |
mulligan |
more slides added, only got topic of changes merged back into o'caml …
|
|
|
@1815
|
9 years |
mulligan |
Added more to talk
|
|
|
@1814
|
9 years |
mulligan |
renamed file to avoid confusion
|
|
|
@1813
|
9 years |
mulligan |
Added presentation that I have been working on for Paris meeting next week.
|
|
|
@1812
|
9 years |
campbell |
Provide a combined type for terminating and non-terminating structured …
|
|
|
@1811
|
9 years |
boender |
- corrected definition of geb
|
|
|