Skip to content
GitLab
Explore
Sign in
Iris
Merge requests
Open
49
Merged
1,756
Closed
208
All
2,013
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
{{title}}
Title
Prove that non-value WP is contractive.
iris!316
· created
Oct 07, 2019
by
Robbert Krebbers
Merged
5
updated
Oct 11, 2019
Prove that invariants are "except 0".
iris!897
· created
Mar 01, 2023
by
Robbert Krebbers
Merged
6
updated
Mar 03, 2023
prove take_0
stdpp!209
· created
Jan 11, 2021
by
Ralf Jung
Merged
1
updated
Jan 11, 2021
Prove stepping (i.e., non-value) version of `atomic_wp_seq`.
iris!402
· created
Mar 25, 2020
by
Robbert Krebbers
Merged
1
5
updated
Mar 25, 2020
prove stack history spec
gpfsl!19
· created
Sep 07, 2021
by
Jaehwang Jung
graphs_multi
Merged
22
updated
Oct 18, 2021
prove stack abstract state spec with history spec
gpfsl!29
· created
Nov 04, 2021
by
Jaehwang Jung
graphs_multi
Merged
1
updated
Nov 05, 2021
prove spsc example with queue graph spec
gpfsl!25
· created
Oct 25, 2021
by
Jaehwang Jung
graphs_multi
Merged
9
updated
Oct 26, 2021
Prove sigT_equivI is admissible (fix #250)
iris!280
· created
Jun 24, 2019
by
Paolo G. Giarrusso
Merged
12
updated
Nov 24, 2020
Prove queue SPMC message passing
gpfsl!27
· created
Oct 27, 2021
by
Jaehwang Jung
graphs_multi
Merged
5
updated
Oct 27, 2021
Prove queue sequential spec
gpfsl!8
· created
Jun 18, 2021
by
Jaemin Choi
graphs_multi
Merged
Approved
7
updated
Jun 20, 2021
prove NoDup_fmap_2_strong
stdpp!173
· created
Jul 07, 2020
by
Ralf Jung
Merged
2
updated
Jul 15, 2020
Prove more equivalences for closure operators on relations.
stdpp!278
· created
Jun 10, 2021
by
Robbert Krebbers
Merged
14
updated
Jun 16, 2021
prove model for own_ptr
lambda-rust!18
· created
Mar 01, 2021
by
Xavier Denis
rusthornbelt
Merged
3
updated
Mar 02, 2021
Prove missing fractional_big_sepL2
iris!737
· created
Oct 01, 2021
by
Paolo G. Giarrusso
Merged
20
updated
Dec 09, 2021
prove map_size_delete, map_size_insert_Some, map_to_list_delete
stdpp!208
· created
Jan 11, 2021
by
Ralf Jung
Merged
11
updated
Jan 11, 2021
prove later commuting around equality one way
iris!388
· created
Mar 06, 2020
by
Ralf Jung
Merged
11
updated
Mar 15, 2020
Prove internal_eq_timeless
iris!607
· created
Dec 19, 2020
by
Paolo G. Giarrusso
Merged
19
updated
Jan 06, 2021
prove general fmap_inj lemmas
stdpp!496
· created
Aug 10, 2023
by
Ralf Jung
Merged
4
updated
Oct 06, 2023
Prove event_list_helper lemmas
gpfsl!7
· created
Jun 11, 2021
by
Jaemin Choi
graphs_multi
Merged
Approved
3
updated
Jun 11, 2021
Prove different versions of Löb rule
iris!451
· created
May 25, 2020
by
Robbert Krebbers
Merged
1
updated
May 25, 2020
Prev
1
…
24
25
26
27
28
29
30
31
32
…
101
Next