

@2428

7 years 
campbell 
Tighten requirements on switch statements in Clight to only give …



@2392

7 years 
campbell 
Labelling translations of && and  need a lot of cost labelling to …



@2391

7 years 
campbell 
Revert "Put the postloop cost label into the Clight while statement …



@2353

7 years 
campbell 
Put the postloop cost label into the Clight while statement to get …



@2338

7 years 
campbell 
Use much nicer definition for making several steps in the labelling …



@2319

7 years 
campbell 
Generate perprogram cost labels rather than perfunction ones, and …



@2203

8 years 
campbell 
A general result about simulations of executions.



@2202

8 years 
campbell 
Start defining equivalent executions.



@2176

8 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@2145

8 years 
campbell 
Cost labelling doesn't affect interaction.



@2134

8 years 
campbell 
Split out behavioural equivalence spec for labelling.



@2118

8 years 
campbell 
Labelling preserves behaviour.



@2107

8 years 
campbell 
Memory initialisation and program transformations.



@2105

8 years 
campbell 
Show some results about globalenvs and program transformations.



@2103

8 years 
campbell 
Make transform_*program take a more general transformation to make …



@2050

8 years 
campbell 
Limit some normalization that doesn't seem to like.



@2019

8 years 
campbell 
Split out special induction principle for Clight from soundness file. …



@2011

8 years 
garnier 
Minor cleanup.



@2000

8 years 
campbell 
Fix g.e. glitch in label simulation.



@1986

8 years 
campbell 
Get rid of unused abstraction of Globalenvs.



@1954

8 years 
campbell 
Initial state is in the labelling simulation
(modulo global envs results).



@1930

8 years 
campbell 
Tidy up labelling simulation stuff a bit.



@1922

8 years 
campbell 
Main labelling simulation proof complete.



@1920

8 years 
campbell 
Most of the labelling simulation. Still need to sort out switch …



@1893

8 years 
campbell 
Show stronger result about labelling of expressions.



@1888

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