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
9 years
campbell
Remove memory spaces other than XData and Code; simplify pointers as a …
(edit)
@2145
9 years
campbell
Cost labelling doesn't affect interaction.
(edit)
@2134
9 years
campbell
Split out behavioural equivalence spec for labelling.
(edit)
@2118
9 years
campbell
Labelling preserves behaviour.
(edit)
@2107
9 years
campbell
Memory initialisation and program transformations.
(edit)
@2105
9 years
campbell
Show some results about globalenvs and program transformations.
(edit)
@2103
9 years
campbell
Make transform_*program take a more general transformation to make …
(edit)
@2050
9 years
campbell
Limit some normalization that
doesn't seem to like.
(edit)
@2019
9 years
campbell
Split out special induction principle for Clight from soundness file. …
(edit)
@2011
9 years
garnier
Minor cleanup.
(edit)
@2000
9 years
campbell
Fix g.e. glitch in label simulation.
(edit)
@1986
9 years
campbell
Get rid of unused abstraction of Globalenvs.
(edit)
@1954
9 years
campbell
Initial state is in the labelling simulation (modulo global envs results).
(edit)
@1930
9 years
campbell
Tidy up labelling simulation stuff a bit.
(edit)
@1922
9 years
campbell
Main labelling simulation proof complete.
(edit)
@1920
9 years
campbell
Most of the labelling simulation. Still need to sort out switch …
(edit)
@1893
9 years
campbell
Show stronger result about labelling of expressions.
(add)
@1888
9 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