-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathindex.html
More file actions
267 lines (267 loc) · 15 KB
/
index.html
File metadata and controls
267 lines (267 loc) · 15 KB
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
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<title>Kasper Svendsen</title>
<link rel="stylesheet" type="text/css" href="style.css" />
</head>
<body>
<div class="main">
<div class="width">
<div class="section">
<div class="content">
<div class="publication">
<div class="pub-title">A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/parallelization-lr.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left"><span class="pub-author">Morten Krogh-Jespersen</span>, <span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Lars Birkedal</span></div>
<div class="right">
<div class="links">
POPL 2017
</div>
</div>
<div style="clear: both"></div>
</div>
We present a relational model of an advanced type-and-effect system that validates advanced type-based equivalences, such as parallelization.
<div class="pub-download">
</div>
</div>
</div>
</div>
<div class="publication">
<div class="pub-title">Verifying Custom Synchronisation Constructs Using Higher-Order Separation Logic</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/custom-sync.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left"><span class="pub-author">Mike Dodds</span>, <span class="pub-author">Suresh Jagannathan</span>, <span class="pub-author">Matthew Parkinson</span>, <span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Lars Birkedal</span></div>
<div class="right">
<div class="links">
TOPLAS
</div>
</div>
<div style="clear: both"></div>
</div>
This paper examines the formal specification and verification of custom synchronisation constructs. Our target is a library of channels used in automated parallelization to enforce sequential behaviour between program statements.
<div class="pub-download">
<a href="articles/custom-sync.pdf">article</a>
</div>
</div>
</div>
</div>
<div class="publication">
<div class="pub-title">Transfinite Step-indexing: Decoupling Concrete and Logical Steps</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/transfinite-lr.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left"><span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Filip Sieczkowski</span>, <span class="pub-author">Lars Birkedal</span></div>
<div class="right">
<div class="links">
ESOP 2016
</div>
</div>
<div style="clear: both"></div>
</div>
Step-indexing is a powerful technique for stratifying the construction of recursive models of advanced type systems and logics. Current techniques enforce a tight coupling between concrete steps and unfoldings of this underlying recursive equation. We show how to weaken this coupling using transfinite step-indexing.
<div class="pub-download">
<a href="articles/transfinite-lr.pdf">article</a> | <a href="transfinite-tr.pdf">technical report</a>
</div>
</div>
</div>
</div>
<div class="publication">
<div class="pub-title">A Separation Logic for Fictional Sequential Consistency</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/icap-tso.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left"><span class="pub-author">Filip Sieczkowski</span>, <span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Lars Birkedal</span>, <span class="pub-author">Jean Pichon-Pharabod</span></div>
<div class="right">
<div class="links">
ESOP 2015
</div>
</div>
<div style="clear: both"></div>
</div>
We present a program logic for a high-level programming language with a weak memory model that supports both low-level reasoning about racy code and high-level reasoning about well-behaved code.
<div class="pub-download">
<a href="articles/icap-tso.pdf">article</a> | <a href="talks/tso-yak.pdf">talk (concurrency yak)</a>
</div>
</div>
</div>
</div>
<div class="publication">
<div class="pub-title">Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/iris.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left"><span class="pub-author">Ralf Jung</span>, <span class="pub-author">David Swasey</span>, <span class="pub-author">Filip Sieczkowski</span>, <span class="pub-author">Kasper Svendsen</span>, <br/><span class="pub-author">Aaron Turon</span>, <span class="pub-author">Lars Birkedal</span>, <span class="pub-author">Derek Dreyer</span></div>
<div class="right">
<div class="links">
POPL 2015
</div>
</div>
<div style="clear: both"></div>
</div>
We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express—and invariants enable us to enforce—user-defined protocols on shared state, which are at the conceptual core of most recent program logics for concurrency.
<div class="pub-download">
<a href="http://plv.mpi-sws.org/iris/">iris</a> | <a href="talks/iris-cambridge.pdf">talk (cambridge lunch talk)</a>
</div>
</div>
</div>
</div>
<div class="publication">
<div class="pub-title">impredicative Concurrent Abstract Predicates</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/icap.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left"><span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Lars Birkedal</span></div>
<div class="right">
<div class="links">
ESOP 2014
</div>
</div>
<div style="clear: both"></div>
</div>
We present a program logic for modular reasoning about safety properties of concurrent, higher-order, reentrant, imperative code.
<div class="pub-download">
<a href="https://bitbucket.org/logsem/public/src/master/icap/esop2014.pdf">article</a> | <a href="https://bitbucket.org/logsem/public/src/master/icap/esop2014-appendix.pdf">appendix</a> | <a href="https://bitbucket.org/logsem/public/src/master/icap/esop2014-tr.pdf">technical report</a> | <a href="talks/hope2013.pdf">talk (hope 2013)</a> | <a href="talks/esop2014.pdf">talk (esop 2014)</a>
</div>
</div>
</div>
</div><div class="publication">
<div class="pub-title">Joins: A Case Study in Modular Specification of a Concurrent Reentrant Library</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/joins.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left">
<span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Lars Birkedal, <span class="pub-author"> Matthew Parkinson</span>
</div>
<div class="right">
<div class="links">
<span class="pub-conf">ECOOP 2013</span>
</div>
</div>
<div style="clear: both"></div>
</div>
We formally specify and verify a lock-based implementation of the C# Joins library using our HOCAP logic.
<div style="text-align: right; font-size: 10pt; margin-top: 15px">
<a href="articles/joins.pdf">article</a> | <a href="articles/joins-tr.pdf">technical report</a> | <a href="talks/hope2012.pdf">talk (hope 2012)</a>
</div>
</div>
</div>
</div><div class="publication">
<div class="pub-title">Modular Reasoning about Separation of Concurrent Data Structures</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/hocap.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left">
<span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Lars Birkedal</span>, <span class="pub-author">Matthew Parkinson</span>
</div>
<div class="right">
<span class="pub-conf">ESOP 2013</span>
</div>
<div style="clear: both"></div>
</div>
We present a spec. pattern for concurrent data structures that is independent of how clients intend to use instances of the data structure.
<div class="pub-download">
<a href="articles/hocap.pdf">article</a> | <a href="articles/hocap-ext.pdf">extended version</a> | <a href="articles/hocap-tr.pdf">technical report</a> | <a href="talks/esop2013.pdf">talk</a>
</div>
</div>
</div>
</div><div class="publication">
<div class="pub-title">Partiality, State, and Dependent Types</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/ihtt.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left">
<span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Lars Birkedal</span>, <span class="pub-author">Aleksandar Nanevski</span>
</div>
<div class="right">
<span class="pub-conf">TLCA 2011</span>
</div>
<div style="clear: both"></div>
</div>
We present a new approach to admissibility for dependent type theories extended with partial types.
<div class="pub-download">
<a href="articles/ihtt.pdf">article</a> | <a href="articles/ihtt-ext.pdf">extended version</a> | <a href="coq/ihtt.tgz">coq code</a> | <a href="talks/tlca2011.pdf">talk</a>
</div>
</div>
</div>
</div><div class="publication">
<div class="pub-title">Verifying Generics and Delegates</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/delegates.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left">
<span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Lars Birkedal</span>, <span class="pub-author">Matthew Parkinson</span>
</div>
<div class="right">
<span class="pub-conf">ECOOP 2010</span>
</div>
<div style="clear: both"></div>
</div>
We present a program logic for a subset of C# that includes generics and anonymous delegates with variable capture.
<div class="pub-download">
<a href="articles/delegates.pdf">article</a> | <a href="articles/delegates-tr.pdf">technical report</a> | <a href="talks/ecoop2010.pdf">talk</a>
</div>
</div>
</div>
</div><div class="publication">
<div class="pub-title">Design Patterns in Separation Logic</div>
<div class="pub-container">
<div class="pub-icon">
<img src="icons/patterns.png"/>
</div>
<div class="pub-desc">
<div class="pub-header">
<div class="left">
<span class="pub-author">Neel Krishnaswami</span>, <span class="pub-author">Jonathan Aldrich</span>, <span class="pub-author">Lars Birkedal</span>, <span class="pub-author">Kasper Svendsen</span>, <span class="pub-author">Alexandre Buisse</span>
</div>
<div class="right">
<span class="pub-conf">TLDI 2009</span>
</div>
<div style="clear: both;"></div>
</div>
We present separation logic specifications for a number of classic design patterns including the subject-observer pattern, the flyweight pattern and the iterator pattern.
<div class="pub-download">
<a href="articles/designpats.pdf">article</a> | <a href="articles/designpats-tr.pdf">technical report</a> | <a href="coq/patterns.tgz">coq code</a>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</body>
</html>