source: src/ASM/Policy.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2230   8 years sacerdot Glue proof maximally simplified or sort of.
(edit) @2229   8 years sacerdot More cleaning up, ready for more aggressive factorization.
(edit) @2228   8 years sacerdot Further proof reduction.
(edit) @2225   8 years sacerdot Minor and major improvements everywhere, shortened proofs.
(edit) @2211   8 years boender - finished proof of sigma specification - added some stuff to Util, as …
(edit) @2153   8 years boender - updated the proof some more
(edit) @2152   8 years boender - this should compile
(edit) @2141   8 years boender - committed working version
(edit) @2101   8 years boender - renamed medium to absolute jump - revised proofs of policy, some …
(edit) @2078   8 years sacerdot sigma_policy_specification has been 1) strengthened 2) made nicer to …
(edit) @2059   8 years boender - updated Policy to work better
(edit) @2055   8 years sacerdot Warning: this commit adds an hypothesis that breaks all of assembly stuff.
(edit) @2034   8 years boender - split Policy into three separate files for ease (and indeed …
(edit) @2032   8 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
(edit) @2018   8 years mulligan CJNE case a complete mess.
(edit) @2008   8 years boender - substantial closing of holes in proof
(edit) @1973   8 years boender - removed superfluous match - displaced 'cases daemon'
(edit) @1965   8 years boender - further completed proof, changed jump_expansion' to reflect new type …
(edit) @1956   8 years boender - finished proof of lemma (where auto does strange things again)
(edit) @1950   8 years boender - advances in policy
(edit) @1942   8 years mulligan Work on showing the equivalence of two methods of looking up from the maps.
(edit) @1940   8 years boender - committed new version of final invariant
(edit) @1937   8 years boender - filled in some of the gaps in the proof of Policy - reverted …
(edit) @1934   8 years boender - various & sundry moves of lemmas to better places - integrated …
(edit) @1933   8 years boender - slight revamp
(edit) @1932   8 years boender - added some more dependent types (we love 'em)
(edit) @1931   8 years boender - added latest bvt alias - temporary "cases daemon" commit of new …
(edit) @1886   8 years boender - improvements for disambiguation and quick(er) typing
(edit) @1879   8 years boender - Policy compiles until the end, still some (fairly trivial) cases …
(edit) @1810   8 years boender - new version of policy that compiles up to the final glue
(edit) @1809   8 years boender - committed partially compiling version of policy (up until …
(edit) @1615   9 years sacerdot Policy now depends on Assembly and not the other way around.
(add) @1614   9 years boender - split policy from assembly
Note: See TracRevisionLog for help on using the revision log.