source: src/common/FEMeasurable.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3007   8 years campbell Sketch out how Cminor to RTLabs correctness would fit into the …
(edit) @2990   8 years campbell Replace dodgy hypothesis by nice ones, clean up a little.
(edit) @2989   8 years campbell Make front-end measurability preservation proof cope with moving the …
(edit) @2953   8 years campbell Fix silly label handling bug I realised was there during my talk…
(edit) @2727   8 years campbell Remove a couple of redundant hypotheses.
(edit) @2726   8 years campbell Show max stack preserved in FEMeasurable.
(edit) @2725   8 years campbell Add observables to FEMeasurable proof; fix silly typo.
(edit) @2690   8 years campbell Most of the measurable subtrace preservation proof done.
(edit) @2685   8 years campbell Progress on measurable trace preservation: prefix preserves observable …
(edit) @2678   8 years campbell Switch to single source step simulations for front-end measurable …
(edit) @2670   8 years campbell Clean up from recent commits.
(edit) @2669   8 years campbell Tweak exec_steps output; show that simulations extend to measurable …
(edit) @2668   8 years campbell Intermediate measurable proof check-in before I change its traces again.
(edit) @2644   8 years campbell Commit some work on FEMeasurable before trying to do something nicer …
(edit) @2618   8 years campbell Tidy up measurable a little.
(add) @2597   8 years campbell Some work in progress on measurable subtrace preservation.
Note: See TracRevisionLog for help on using the revision log.