Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
source:
src
/
common
/
SmallstepExec.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)
@2668
7 years
campbell
Intermediate measurable proof check-in before I change its traces again.
(edit)
@2618
7 years
campbell
Tidy up measurable a little.
(edit)
@2487
7 years
campbell
Set up "after_n_steps" to enforce an invariant on states.
(edit)
@2459
7 years
campbell
Syntax update
(edit)
@2444
7 years
campbell
Some inversion lemmas for after_n_steps for dealing with >1 source …
(edit)
@2338
7 years
campbell
Use much nicer definition for making several steps in the labelling …
(edit)
@2203
8 years
campbell
A general result about simulations of executions.
(edit)
@2202
8 years
campbell
Start defining equivalent executions.
(edit)
@2145
8 years
campbell
Cost labelling doesn't affect interaction.
(edit)
@2118
8 years
campbell
Labelling preserves behaviour.
(edit)
@1599
8 years
sacerdot
Start of merging of stuff into the standard library of Matita.
(edit)
@1233
8 years
sacerdot
1) Ported to Brian's new dependent type for fullexec 2) Universe level …
(edit)
@1231
8 years
campbell
Change
SmallstepExec?
so that states can depend on global information. …
(edit)
@1213
8 years
sacerdot
1) New values (joint/BEValues.ma) and memory model for the back-ends …
(edit)
@1181
8 years
mulligan
changed smallstep exec in order to remove matita bug (superposition.ml …
(edit)
@797
9 years
campbell
Add error messages wherever the error monad is used. Sticks to …
(edit)
@751
9 years
campbell
Initial version of the Cminor syntax and semantics.
(edit)
@731
9 years
campbell
Common definition for animation semantics, and factor out IO definitions.
(edit)
@702
9 years
campbell
Refine small-step executable semantics abstraction a little. Some …
(edit)
@700
9 years
campbell
Get Clight semantics going again (except for problems
CexecEquiv?
that …
(copy)
@695
9 years
campbell
Rearrange Clight files a bit - will try to make them work again soon…
copied from
src/Clight/SmallstepExec.ma
:
(copy)
@694
9 years
campbell
Start moving Clight into common directory.
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog