Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
source:
src
/
Clight
/
labelSimulation.ma
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@2176
8 years
campbell
Remove memory spaces other than XData and Code; simplify pointers as a …
(edit)
@2145
8 years
campbell
Cost labelling doesn't affect interaction.
(edit)
@2134
8 years
campbell
Split out behavioural equivalence spec for labelling.
(edit)
@2118
8 years
campbell
Labelling preserves behaviour.
(edit)
@2107
8 years
campbell
Memory initialisation and program transformations.
(edit)
@2105
8 years
campbell
Show some results about globalenvs and program transformations.
(edit)
@2103
8 years
campbell
Make transform_*program take a more general transformation to make …
(edit)
@2050
8 years
campbell
Limit some normalization that
doesn't seem to like.
(edit)
@2019
8 years
campbell
Split out special induction principle for Clight from soundness file. …
(edit)
@2011
8 years
garnier
Minor cleanup.
(edit)
@2000
8 years
campbell
Fix g.e. glitch in label simulation.
(edit)
@1986
8 years
campbell
Get rid of unused abstraction of Globalenvs.
(edit)
@1954
8 years
campbell
Initial state is in the labelling simulation (modulo global envs results).
(edit)
@1930
8 years
campbell
Tidy up labelling simulation stuff a bit.
(edit)
@1922
8 years
campbell
Main labelling simulation proof complete.
(edit)
@1920
8 years
campbell
Most of the labelling simulation. Still need to sort out switch …
(edit)
@1893
8 years
campbell
Show stronger result about labelling of expressions.
(add)
@1888
8 years
campbell
Show that labelling of expressions works ... after fixing it to match …
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog