Merge requests · Iris / Iris · GitLab

Add order operations for locations in HeapLang.

!854 · created Oct 14, 2022 by Arthur Azevedo de Amorim S-waiting-for-author
- 6
updated Nov 23, 2022
Add comments to explain the modified structure of the adequacy proof

!847 · created Aug 19, 2022 by Simon Spies S-waiting-for-author
- MERGED
- 17
updated Feb 01, 2023
Allow controlling stuckness at the language level 0 of 6 checklist items completed

!825 · created Aug 02, 2022 by Michael Sammler S-waiting-for-author
- 56
updated Nov 23, 2022
make Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails)

!791 · created May 07, 2022 by Ralf Jung S-waiting-for-author
- 29
updated Dec 05, 2022
Attempt at avoiding `unfold` to unfold primitive projections. 2 of 3 checklist items completed

!778 · created Feb 14, 2022 by Robbert Krebbers S-waiting-for-author
- 14
updated May 18, 2022
Updated suggested emacs indendation configuration

!776 · created Jan 19, 2022 by Jonas Kastberg S-waiting-for-author
- MERGED
- 18
updated May 11, 2022
Draft: Add simple library for priority levels and use it for `iFrame`

!742 · created Oct 11, 2021 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 18
updated May 06, 2022
WIP: Define more uPred connectives in siProp

!710 · created Jun 29, 2021 by Hai Dang S-draft S-waiting-for-author
- CLOSED
- 55
updated Nov 30, 2021
Add mode for Dist

!700 · created Jun 08, 2021 by Paolo G. Giarrusso S-waiting-for-author
- MERGED
- 23
updated Jun 18, 2021
Add generalized implication lemma for big_sepM

!697 · created Jun 01, 2021 by Simon Friis Vindum S-waiting-for-author
- MERGED
- 57
updated Jul 31, 2021
Add missing commutations for `fupd`

!688 · created May 21, 2021 by Paolo G. Giarrusso S-waiting-for-author
- MERGED
- 30
updated May 31, 2021
Draft: More (peri)scopes for Iris

!651 · created Mar 16, 2021 by Paolo G. Giarrusso S-waiting-for-author
- CLOSED
- 18
updated May 07, 2021
Alternative take at "better support for view shift with mismatching masks"

!615 · created Jan 05, 2021 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 6
updated Apr 29, 2021
Use class `IntoFUpd` in tactic `wp_value_head`

!613 · created Jan 05, 2021 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 13
updated Dec 12, 2021
Add a verified interpreter for HeapLang

!564 · created Nov 03, 2020 by Tej Chajed S-waiting-for-author
- MERGED
- 43
updated Mar 18, 2021
WIP: Prototype a validity restriction CMRA construction

!502 · created Sep 08, 2020 by Tej Chajed S-waiting-for-author
- CLOSED
- 24
updated Sep 14, 2020
Define logic `clProp` for axiom-free classical logic

!496 · created Sep 05, 2020 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 45
updated May 12, 2021
if instances for absorbing, affine and persistent

!474 · created Jul 13, 2020 by Alix Trieu S-waiting-for-author
- CLOSED
- 8
updated Sep 08, 2020
WIP: Add `with M` option to `iModIntro` and use to redefine `iNext` to fix issue #331

!467 · created Jun 29, 2020 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 41
updated Sep 29, 2020
Specify how to compile Iris without running the tests

!466 · created Jun 19, 2020 by Dan Frumin S-waiting-for-author
- CLOSED
- 13
updated Sep 30, 2020