Merge Requests · Iris

Logical Relations

actris!3 · opened Apr 02, 2020 by Jonas Kastberg
- MERGED
- 1
- 65
updated Apr 06, 2020
drop_insert -> drop_insert_gt

iris!407 · opened Mar 31, 2020 by Michael Sammler
- MERGED
- 1
- 1
updated Mar 31, 2020
Spell check proof_guide.md

iris!405 · opened Mar 27, 2020 by Paolo G. Giarrusso
- MERGED
- 1
- 1
updated Mar 27, 2020
Prove stepping (i.e., non-value) version of `atomic_wp_seq`.

iris!402 · opened Mar 25, 2020 by Robbert Krebbers
- MERGED
- 1
- 5
updated Mar 25, 2020
Subprotocols with message swapping

actris!2 · opened Mar 25, 2020 by Robbert Krebbers
- MERGED
- 1
- 2
updated Mar 25, 2020
Fix `Export` order for `length`. Remove `length` hack in strings.

stdpp!129 · opened Mar 24, 2020 by Robbert Krebbers
- MERGED
- 1
- 28
updated Apr 11, 2020
Close issue #299: `leibnizO` finds convoluted proof for definitions

iris!392 · opened Mar 12, 2020 by Robbert Krebbers
- MERGED
- 1
- 6
updated Mar 12, 2020
Fix discrepancies in bi notations.

iris!384 · opened Feb 24, 2020 by Robbert Krebbers
- MERGED
- 1
- 16
updated Mar 30, 2020
Derive WP lifting and array rules from TWP rules

iris!383 · opened Feb 23, 2020 by Robbert Krebbers
- MERGED
- 1
- 31
updated Feb 25, 2020
Add ownership fraction to array assertion

iris!380 · opened Feb 22, 2020 by Tej Chajed
- MERGED
- 1
- 25
updated Feb 23, 2020
drop support for Coq 8.8

iris!378 · opened Feb 19, 2020 by Ralf Jung
- MERGED
- 1
- 4
updated Mar 13, 2020
say things about modalities

iris!377 · opened Feb 18, 2020 by Ralf Jung
- MERGED
- 1
- 14
updated Feb 20, 2020
heap_lang/lifting.v: Don't run auto on hopeless goals

iris!369 · opened Feb 04, 2020 by Paolo G. Giarrusso
- MERGED
- 1
- 1
updated Feb 05, 2020
Disclaimer for STSs.

iris!366 · opened Jan 30, 2020 by Robbert Krebbers
- MERGED
- 1
- 3
updated Jan 30, 2020
fix big_sepM2_fmap and friend to work for keys other than nat

iris!351 · opened Dec 20, 2019 by Michael Sammler
- MERGED
- 1
- 2
updated Dec 20, 2019
Use &&& from lazy_bool_scope instead of redefining the && notation.

iris!349 · opened Dec 18, 2019 by Jacques-Henri Jourdan
- MERGED
- 1
- 0
updated Jan 09, 2020
Add `Atomic` instances for all atomic `heap_lang` constructs.

iris!317 · opened Oct 12, 2019 by Robbert Krebbers
- MERGED
- 1
- 6
updated Oct 14, 2019
Soundness lemma for internal equality of `uPred`.

iris!315 · opened Sep 23, 2019 by Robbert Krebbers
- MERGED
- 1
- 2
updated Dec 05, 2019
More lemmas for `filter` w.r.t. maps

stdpp!96 · opened Sep 11, 2019 by Robbert Krebbers
- MERGED
- 1
- 2
updated Sep 12, 2019
Add `iStopProof` tactic

iris!311 · opened Sep 07, 2019 by Robbert Krebbers
- MERGED
- 1
- 8
updated Sep 19, 2019