aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/AbstractInterpretation.v
Commit message (Expand)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* Guarantee that casting always returns inrangeGravatar Jason Gross2018-10-12
* Fix and prove bounds for fancymachine operationsGravatar jadep2018-09-28
* Finish interp proof of abstract interpretationGravatar Jason Gross2018-09-14
* Fix some bounds analysisGravatar Jason Gross2018-08-13
* Fix a wrong bound computation (on negatives), fix a proofGravatar Jason Gross2018-08-13
* Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool...Gravatar Jason Gross2018-08-13
* Don't guarantee anything about casting outside of rangeGravatar Jason Gross2018-08-10
* Don't fuse annotationsGravatar Jason Gross2018-08-09
* Push back admits in interp lemmasGravatar Jason Gross2018-08-08
* Finish relax interp proofsGravatar Jason Gross2018-08-07
* Add another GeneralizeVar pass to add support for using Wf3Gravatar Jason Gross2018-08-07
* Remove fastpath for Zcast in absintGravatar Jason Gross2018-08-06
* Remove thunking from abstract interpretationGravatar Jason Gross2018-08-06
* Allow proving force ∘ thunk = id extensionallyGravatar Jason Gross2018-07-30
* Support reification of firstn, skipnGravatar Jason Gross2018-07-18
* Allow reification of nat_rect (fun _ => _ -> _)Gravatar Jason Gross2018-07-15
* Correctly reify match on prodGravatar Jason Gross2018-07-03
* WIPGravatar Jason Gross2018-07-03
* New pipeline, split among filesGravatar Jason Gross2018-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 05:08:51 +0000