forked from logsem/iris-project
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
314 lines (283 loc) · 13.8 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
---
---
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
<meta name="description" content="">
<meta name="author" content="">
<meta name="referrer" content="origin-when-cross-origin">
<title>Iris Project</title>
<link rel="stylesheet" href="bootstrap.min.css" integrity="sha384-rbsA2VBKQhggwzxH7pPCaAqO46MgnOM80zW1RWuH61DGLwZJEdK2Kadq2F9CUG65" crossorigin="anonymous">
<link rel="stylesheet" href="style.css">
<link rel="icon" type="image/svg+xml" href="gfx/favicon.svg">
<link rel="alternate icon" href="gfx/favicon.ico">
</head>
<body>
<div class="container-fluid">
<div class="bg-secondary py-5 mb-3 text-sm-center" style="--bs-bg-opacity : 0.1">
<div class="container-fluid">
<img src="gfx/logo.svg" style="height:140px; margin-bottom:30px;" alt="Iris logo">
<p class="lead">A Higher-Order Concurrent Separation Logic Framework, <br> implemented and verified in the Coq
proof assistant</p>
<p>
<a href="https://gitlab.mpi-sws.org/iris/iris/" class="btn btn-primary">Coq Formalization</a>
<a href="https://plv.mpi-sws.org/iris/appendix-4.2.pdf" class="btn btn-primary">Technical Reference (v4.2)</a>
<a href="https://lists.mpi-sws.org/listinfo/iris-club" class="btn btn-primary">Mailing List</a>
<a href="chat.html" class="btn btn-primary">Chat</a>
</p>
<p>
<a href="#learning" class="btn btn-light border" role="button">Learning Iris</a>
<a href="#events" class="btn btn-light border" role="button">Events</a>
<a href="#publications" class="btn btn-light border" role="button">Publications</a>
<a href="#phd" class="btn btn-light border" role="button">PhD dissertations</a>
<a href="#other" class="btn btn-light border" role="button">Other material</a>
</p>
</div>
</div>
<div class="container">
<div class="container">
<div>
<p>
Iris is a framework that can be used for reasoning about
safety of concurrent programs, as the logic in logical
relations, to reason about type-systems, data-abstraction
etc.
In case of questions, please contact us on the <a href="https://lists.mpi-sws.org/listinfo/iris-club">Iris
Club
list</a> or in our <a href="chat.html">chat room</a>.
</div>
</div>
<div class="container" style="margin-bottom: 20px;">
<div>
<a name="learning"></a>
<h2>Learning Iris</h2>
</div>
<div>
<p>Some useful resources designed to learn Iris and its Coq implementation:</p>
<ul>
<li>The <a href="tutorial-material.html">Iris lecture notes</a> provide a tutorial style introduction to
Iris,
including a number of exercises (but most of it not in Coq).</li>
<li>The second half of Derek Dreyer's <a href="https://plv.mpi-sws.org/semantics-course/">Semantics lecture
notes</a> gives an introduction to Iris, including exercises and a Coq development.</li>
<li>The <a href="https://gitlab.mpi-sws.org/iris/tutorial-popl21">Iris Tutorial at POPL'21</a> contains a
number
of exercises to practice the Iris tactics in Coq. A <a
href="https://www.youtube.com/watch?v=LjXaffBpMag">video recording</a> of the tutorial talk is also
available.</li>
<li>The paper <a href="pdfs/2024-submitted-logical-type-soundness.pdf">A Logical Approach to Type
Soundness</a>
shows how Iris can be used to prove type soundness. See also the <a
href="https://www.youtube.com/watch?v=8Xyk_dGcAwk">video recording</a> of Derek Dreyer's POPL'18 keynote
and
the
<a href="https://gitlab.mpi-sws.org/iris/tutorial-popl20">Iris Tutorial at POPL'20</a>.
</ul>
<p>A selection of papers that are suited to get started with Iris:</p>
<ul>
<li>The <a href="https://www.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf">Iris From The Ground Up
paper</a> contains an extensive description of the rules and the model of the Iris logic.</li>
<li>The <a href="pdfs/2017-popl-proofmode-final.pdf">Iris Proofmode paper (Section 3)</a> contains a brief
tutorial to the Iris tactics in Coq.</li>
<li>The <a href="https://gitlab.mpi-sws.org/iris/iris/blob/master/docs/proof_mode.md">Iris Proof Mode (IPM)
/
MoSeL</a> and the <a
href="https://gitlab.mpi-sws.org/iris/iris/blob/master/docs/heap_lang.md">HeapLang</a>
documentation provide a reference of the Iris tactics in Coq.</li>
</ul>
</div>
</div>
<div class="container" style="margin-bottom: 20px;">
<div>
<a name="events"></a>
<h2>Events</h2>
<ul>
<li>3 June–7 June 2024: <a href="workshop-2024">The Fourth Iris Workshop</a>, Zürich, Switzerland</li>
<li>15 January 2024: <a
href="https://popl24.sigplan.org/details/POPL-2024-tutorialfest/4/Verified-Message-Passing-Concurrency-in-Iris-Separation-Logic-Meets-Session-Types">Tutorial
on Iris and Session Types</a> at POPL, London, UK</li>
<li>22 May–26 May 2023: <a href="workshop-2023">The Third Iris Workshop</a>, Saarbrücken, Germany</li>
<li>2 May–6 May 2022: <a href="workshop-2022">The Second Iris Workshop</a>, Nijmegen, The Netherlands</li>
<li>18 January 2021: <a
href="https://popl21.sigplan.org/details/POPL-2021-tutorialfest/4/-T4-Iris-A-Modular-Foundation-for-Higher-Order-Concurrent-Separation-Logic">Tutorial
on Iris</a> at POPL, Virtual</li>
<li>20 January 2020: <a
href="https://popl20.sigplan.org/details/POPL-2020-tutorialfest/4/-T4-Proving-Semantic-Type-Soundness-in-Iris">Tutorial
on Proving Semantic Type Soundness in Iris</a> at POPL, New Orleans, USA</li>
<li>28 October–1 November 2019: <a href="workshop-2019">The First Iris Workshop</a>, Aarhus, Denmark</li>
<li>8 January 2018: <a
href="https://popl18.sigplan.org/details/POPL-2018-TutorialFest/1/Iris-A-Modular-Foundation-for-Higher-Order-Concurrent-Separation-Logic-">Tutorial
on Iris</a> at POPL, Los Angeles, USA</li>
</ul>
</div>
</div>
<div class="container" style="margin-bottom: 20px;">
<div>
<a name="publications"></a>
<h2>Publications</h2>
</div>
<div>
<p>Below, we give an overview of the research that uses Iris one way or another.</p>
</div>
<div>
<dl class="ref">
{% include publications.html publications=site.data.publications.publications %}
</dl>
</div>
<div>
<a name="phd"></a>
<h2>PhD dissertations</h2>
</div>
<div>
<dl class="ref">
{% include publications.html publications=site.data.publications.phd_dissertations %}
</dl>
</div>
<div>
<a name="other"></a>
<h2>Other material</h2>
</div>
<div>
<p>Draft papers:</p>
<dl class="ref">
{% include publications.html publications=site.data.publications.draft_papers pdf_name="[preprint] .pdf" %}
</dl>
</div>
<div>
<p>Case studies, MSc theses, abstracts, talks:</p>
<dl class="ref">
{% include publications.html publications=site.data.publications.others %}
</dl>
</div>
</div>
</div>
<div class="bg-secondary py-5 mb-3" style="--bs-bg-opacity : 0.1">
<div class="container">
<h2>Main research groups involved</h2>
<div class="card-group">
<div class="card mx-2 border">
<a href="http://cs.au.dk/" class="card-link" title="Visit Aarhus University">
<img class="card-img-top" style="width : auto; max-width : 80%;" src="gfx/au.png" alt="Aarhus University">
</a>
<div class="card-footer text-muted" style="text-align: center;">
Logic and Semantics Group <br />
<span class="muted" style="font-size: 10pt;">Contact: <a href="http://cs.au.dk/~birke/">Lars
Birkedal</a></span>
</div>
</div>
<div class="card mx-2 border">
<a href="http://www.mpi-sws.org/" class="card-link" title="Visit Max Planck Institute for Software Systems">
<img class="card-img-top" style="width : auto; max-width : 80%;" src="gfx/mpi-sws-logo.svg"
alt="Max Planck Institute for Software Systems" width=250>
</a>
<div class="card-footer text-muted" style="text-align: center;">
Foundations of Programming Group<br />
<span class="muted" style="font-size: 10pt;">Contact: <a href="https://www.mpi-sws.org/~dreyer/">Derek
Dreyer</a></span>
</div>
</div>
<div class="card mx-2 border">
<a href="http://www.ru.nl" class="card-link" title="Visit Radboud University">
<img class="card-img-top" style="width : auto; max-width : 80%;" src="gfx/radboud.jpg"
alt="Radboud University">
</a>
<div class="card-footer text-muted" style="text-align: center;">
Department of Software Science<br />
<span class="muted" style="font-size: 10pt;">Contact: <a href="https://robbertkrebbers.nl">Robbert
Krebbers</a></span>
</div>
</div>
<!-- <div class="card-deck">
<div class="card">
<a href="http://www.tudelft.nl" class="card-link" title="Visit Delft University of Technology">
<img class="card-img-top" src="gfx/delft.png" alt="Delft University of Technology">
</a>
<div class="card-footer text-muted" style="text-align: center;">
Programming Languages Group<br />
<span class="muted" style="font-size: 10pt;">Contact: <a href="https://robbertkrebbers.nl">Robbert Krebbers</a></span>
</div>
</div>
<div class="card">
<a href="http://www.kuleuven.be" class="card-link" title="Visit KU Leuven">
<img class="card-img-top" src="gfx/KU_Leuven.png" alt="KU Leuven">
</a>
<div class="card-footer text-muted" style="text-align: center;">
DistriNet Group<br />
<span class="muted" style="font-size: 10pt;">Contact: <a href="https://distrinet.cs.kuleuven.be/people/amin">Amin Timany</a></span>
</div>
</div>
</div>
-->
</div>
</div>
</div>
<div class="container container-spacing">
<div>
<h2>Grants</h2>
<p class="lead">
The Iris project has been supported by the following grants:
</p>
</div>
<div class="card-group">
<div class="card mx-2 border">
<div class="card-body">
<h4 class="card-title">ModuRes</h4>
<h6 class="card-subtitle text-muted">Modular Reasoning about Concurrent Higher-Order Imperative Programs
</h6>
</div>
<div class="grants">
<img src="https://cs.au.dk/~birke/modures/ModuRes_logo.jpg" alt="Card image">
</div>
<div class="card-body">
<p class="card-text">Grants from The Danish Council for Independent Research, Sapere Aude: DFF–Advanced
Grant 2013
(<a href="http://cs.au.dk/~birke/modures/" class="card-link">more information</a>)</p>
</div>
</div>
<div class="card mx-2 border">
<div class="card-body">
<h4 class="card-title">RustBelt</h4>
<h6 class="card-subtitle text-muted">Logical Foundations for the Future of Safe Systems Programming</h6>
</div>
<div class="grants">
<img src="https://plv.mpi-sws.org/rustbelt/rustbelt_files/rustbelt-icon.png" alt="Card image">
</div>
<div class="card-body">
<p class="card-text">
2015 ERC Consolidator Grant
(<a href="http://plv.mpi-sws.org/rustbelt/" class="card-link">more information</a>)
</p>
</div>
</div>
<div class="card mx-2 border">
<div class="card-body">
<h4 class="card-title">CPV</h4>
<h6 class="card-subtitle text-muted">Center for Basic Research in Program Verification
</h6>
</div>
<div class="grants">
<img src="./gfx/velux.png" alt="The Velux Foundations">
</div>
<div class="card-body">
<p class="card-text">
Villum Investigator grant (no. 25804) from The Villum Foundation from 2019-2025.
(<a href="https://cs.au.dk/research/centers/cpv/" class="card-link">more information</a>)</p>
</div>
</div>
</div>
</div>
</div>
<hr />
<footer style="width: 100%; text-align: center;">
<div class="container">
<span class="text-muted">iris-project.org is maintained by Logic and Semantics group, Computer Science @ Aarhus
University</span>
</div>
</footer>
<script src="/bootstrap.min.js" integrity="sha384-cuYeSxntonz0PPNlHhBs68uyIAVpIIOZZ5JqeqvYYIcEL727kskC66kF92t6Xl2V"
crossorigin="anonymous"></script>
</body>
</html>