Skip to content
GitLab
Explore
Sign in
Iris
Iris
Merge requests
Open
2
Merged
7
Closed
15
All
24
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}}
Milestone due date
`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.
!916
· created
Apr 30, 2023
by
Robbert Krebbers
S-waiting-for-author
6
updated
Jul 25, 2023
Renamed/added macros to iris.sty
!851
· created
Oct 12, 2022
by
Jonas Kastberg
S-waiting-for-author
38
updated
Jul 25, 2023
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
Closed
60
updated
Mar 20, 2023
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
Sep 29, 2023
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
WIP: Remove `contractive_ne` and `contractive_proper` as instances.
!455
· created
May 27, 2020
by
Robbert Krebbers
S-waiting-for-author
Closed
13
updated
Feb 15, 2021
Prev
1
2
Next