Skip to content
GitLab
Explore
Sign in
Iris
Iris
Merge requests
Open
20
Merged
909
Closed
118
All
1,047
Actions
Subscribe to RSS feed
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
WIP: Documentation on Iris equalities
!300
· created
Aug 09, 2019
by
Paolo G. Giarrusso
S-waiting-for-author
Closed
73
updated
Nov 06, 2020
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
WIP: Define bupd in terms of other connectives.
!172
· created
Aug 17, 2018
by
Joseph Tassarotti
Closed
11
updated
Jan 17, 2019
WIP: Changing the definition of contractiveness to be compatible with Transfinite Iris
!616
· created
Jan 11, 2021
by
Simon Spies
S-draft
Closed
43
updated
Nov 30, 2021
WIP: Avoid inG when possible
!219
· created
Feb 20, 2019
by
Ralf Jung
Closed
23
updated
Dec 07, 2020
WIP: Add treiber's stack
!10
· created
Sep 12, 2016
by
Ghost User
Closed
23
updated
Oct 11, 2016
WIP: add sections for ASCII notations
!426
· created
Apr 15, 2020
by
Paolo G. Giarrusso
Closed
4
updated
Jun 23, 2020
WIP: Add persistent points-to predicate to Iris
!493
· created
Aug 23, 2020
by
Simon Friis Vindum
Closed
26
updated
Oct 26, 2020
WIP: Add mk_sync
!4
· created
Aug 12, 2016
by
Ghost User
Closed
12
updated
Aug 27, 2016
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
WIP: A library for (monotone) partial bijections.
!91
· created
Nov 27, 2017
by
Dan Frumin
Closed
12
updated
Dec 18, 2020
WIP ltac_tactics.v show `lazy_tc` does not work
!272
· created
Jun 15, 2019
by
Paolo G. Giarrusso
Closed
2
updated
Jun 18, 2019
WIP Define persistently from the BI interface.
!132
· created
Mar 21, 2018
by
Joseph Tassarotti
gen_proofmode
A-theory
Closed
26
updated
May 31, 2020
when the goal is an evar, pick emp when possible
!139
· created
Apr 20, 2018
by
Ralf Jung
gen_proofmode
Closed
2
updated
Jan 31, 2020
Weakest preconditions for total program correctness
5 of 5 checklist items completed
!65
· created
Sep 24, 2017
by
Robbert Krebbers
Merged
69
updated
Jan 18, 2018
weaken BI axiom persistently_and_sep_elim and re-derive the stronger form
!119
· created
Feb 21, 2018
by
Ralf Jung
gen_proofmode
Merged
0
updated
Feb 21, 2018
Weaken axioms for BI embeddings
!137
· created
Apr 04, 2018
by
Robbert Krebbers
gen_proofmode
Merged
27
updated
Apr 09, 2018
vdash changelog
!393
· created
Mar 16, 2020
by
Ralf Jung
Merged
2
updated
Mar 16, 2020
Various improvements to iFrame
!110
· created
Feb 02, 2018
by
Robbert Krebbers
Merged
19
updated
Feb 08, 2018
various algebra lemmas
!523
· created
Sep 29, 2020
by
Ralf Jung
Merged
0
updated
Sep 29, 2020
Prev
1
2
3
4
5
6
…
53
Next