-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy pathindex.html
More file actions
423 lines (389 loc) · 15.6 KB
/
index.html
File metadata and controls
423 lines (389 loc) · 15.6 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
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
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8"/>
<meta name="viewport" content="width=device-width,initial-scale=1"/>
<title>SPLS, 5 March 2025, Stirling</title>
<style>
BODY {
max-width: 67em; padding: 0; margin: auto;
}
SECTION {
padding-top: 1%;
}
H1, H2, H3, H4, H5, H6, P, TABLE, OL, UL {
padding: 0 3% 0 3%;
margin-left: 0;
margin-right: 0;
margin-bottom: 1%;
}
LI {
margin-left: 1em;
margin-top: 0.5em;
}
LI:first-child {
margin-top: 0.25em;
}
BODY {
font-family: sans-serif;
color: #000020;
background-color: #ffffff;
}
H2, H3 {
font-weight: bold;
color: #000080;
background-color: #d0d0ff;
}
IMG.logo {
vertical-align: middle;
max-height: 72px;
padding: 0 3% 0 3%;
}
.map {
padding: 0 3% 0 3%;
}
TABLE {
color: #f00000;
}
TH {
background-color: #f0f0ff;
}
TD {
color: #200000;
background-color: #f0f0ff;
vertical-align: top;
padding: 1% 1% 1% 1%;
}
TD.author {
padding: 0.5% 1% 0.5% 0.5%;
width: 20em;
}
TD.title {
padding: 0.5% 0.5% 0.5% 1%;
width: 44em;
}
HR {
color: #3030e0;
}
.header {}
.footer {
font-weight: normal;
font-size: smaller;
}
.author {
font-style: normal;
}
.title {
font-style: italic;
}
.abstract {
font-style: normal;
font-size: 95%;
}
.abstract P {
margin: 1% 0 0 0;
}
TD.phdevent {
padding: 0.5% 0.5% 0.5% 1%;
width: 64em;
}
</style>
<script>
function showAbstract(name) {
document.getElementById(name + "/abstract").style.display = "block";
document.getElementById(name + "/button").style.display = "none";
}
function hideAbstract(name) {
document.getElementById(name + "/button").style.display = "block";
document.getElementById(name + "/abstract").style.display = "none";
}
</script>
</head>
<body>
<header>
<h1>Scottish Programming Languages Seminar</h1>
<h2>Wednesday, 5th March 2025</h2>
<p>
The <a href="../../../">Scottish Programming Languages Seminar (SPLS)</a>
is a forum for discussion of all aspects for programming languages.
</p>
<p>
This edition of SPLS will be held as a hybrid event, supporting both
in-person and remote participation.
The in-person meeting will take place in the
<strong>Cottrell Building, room 2A93</strong>
at the <strong>University of Stirling</strong>.
</p>
<p>
This edition of SPLS is sponsored by <a href="https://www.sicsa.ac.uk/">SICSA</a>.
</p>
<div class="header">
<a href="https://www.sicsa.ac.uk/"><img class="logo" src="images/sicsa_blue.jpg" alt="SICSA Logo"></a>
<a href="https://www.stir.ac.uk/"><img class="logo" src="images/stirling.png" alt="University of Stirling Logo" style="height:48px;"></a>
</div>
</header>
<section>
<h3><a name="registration" class="anchor">Registration</a></h3>
<ul>
<li>If you plan to attend in person register <strong>by 25th February</strong> on <a href="https://framadate.org/kdjkNTVpSWOXSWb6">this poll</a>.</li>
<li>Registration is required for catering. Lunch will have plenty of vegetarian options, but if you have other dietary requirements, please use the comments field of the poll or contact the organisers directly.</li>
</ul>
</section>
<section>
<h3><a name="programme" class="anchor">Programme</a></h3>
<h4>12:00 — 13:00 LUNCH</h4>
<h4>13:00 — 14:00 SESSION 1</h4>
<table>
<tr>
<td class="author">
Jan Menz<br/>(Max Planck Institute for Software Systems)
</td>
<td class="title">
<span>
Dependency tracking for higher-order what declassification
</span>
<div class="abstract" id="Jan/button">
<button onclick="showAbstract('Jan')">Abstract</button>
</div>
<div class="abstract" id="Jan/abstract" style="display:none;">
<button onclick="hideAbstract('Jan')">Hide Abstract</button>
<p>
Many programs process secret data. In fact, they often need
to reveal some amount of secret data.
<em>What declassification</em> allows a programmer to specify
what data they are willing to reveal. In this work in progress,
we use dependency tracking to reason about what declassification
in the higher-order setting. We present a novel
dependency-tracking type system tracking dependencies
of expressions on other expressions in their type and
a novel compositional semantics interpreting those types
to give what-declassification guarantees. The heart
of our type system, the „trivial rule“, says that
an expression’s dependency can always be replaced
with the most precise dependency: the expression itself.
</p>
</div>
</td>
</tr>
<tr>
<td class="author">
Orpheas van Rooij<br/>(University of Edinburgh)
</td>
<td class="title">
<span>
Affect: An Affine Type and Effect System
</span>
<div class="abstract" id="Orpheas/button">
<button onclick="showAbstract('Orpheas')">Abstract</button>
</div>
<div class="abstract" id="Orpheas/abstract" style="display:none;">
<button onclick="hideAbstract('Orpheas')">Hide Abstract</button>
<p>
Effect handlers generalise exception handlers, but allow
resumption of the continuation from where the effect was raised.
Allowing continuations to be resumed
at most once (<em>one-shot</em>) or
an arbitrary number of times (<em>multi-shot</em>)
has far-reaching consequences.
In addition to performance considerations, multi-shot effects
break key rules of reasoning and thus render certain standard
transformation/optimizations unsound, especially in languages
with mutable references (such as OCaml 5).
It is therefore desirable to statically track whether
continuations are used in a one-shot or multi-shot discipline,
so that a compiler could use this information to efficiently
implement effect handlers and to determine what optimizations
it may perform.
</p>
<p>
We address this problem by developing a type and effect system
— called <em>Affect</em> —
which uses affine types to track the usage of continuations.
To prove soundness of Affect we model types and judgements
semantically via a logical relation
in the Iris separation logic framework in Rocq.
</p>
</div>
</td>
</tr>
</table>
<h4>14:00 — 14:30 COFFEE</h4>
<h4>14:30 — 15:30 SESSION 2</h4>
<table>
<tr>
<td class="author">
Matthew Alan Le Brun<br/>(University of Glasgow)
</td>
<td class="title">
<span>
Multiparty Session Types with a Bang!
</span>
<div class="abstract" id="Matthew/button">
<button onclick="showAbstract('Matthew')">Abstract</button>
</div>
<div class="abstract" id="Matthew/abstract" style="display:none;">
<button onclick="hideAbstract('Matthew')">Hide Abstract</button>
<p>
Replication is an alternative construct to recursion for
describing infinite behaviours in the pi-calculus. We explore
the implications of including type-level replication in
<em>Multiparty Session Types (MPST)</em>, a behavioural type
theory for message-passing programs. We introduce <em>MPST!</em>,
a session-typed multiparty process calculus with replication
and first-class roles. We find that replication is not an
equivalent alternative to recursion in MPST, and using both
constructs in one type system in fact allows us to express
both context-free protocols and protocols that make
interesting use of <em>mutual exclusion</em> and <em>races</em>.
In this talk, we will demonstrate the expressiveness of
replication in MPST by example, observe the mutual non-inclusion
result, and discuss the decidability of typechecking.
</p>
</div>
</td>
</tr>
<tr>
<td class="author">
Leonid Nosovitskiy<br/>(University of St Andrews)
</td>
<td class="title">
<span>
Multiparty Session Types: Paxos Made Easy
</span>
<div class="abstract" id="Leonid/button">
<button onclick="showAbstract('Leonid')">Abstract</button>
</div>
<div class="abstract" id="Leonid/abstract" style="display:none;">
<button onclick="hideAbstract('Leonid')">Hide Abstract</button>
<p>
Multiparty Session Types (MPST) offer a robust framework
to ensure indispensable properties in distributed systems.
However, their adoption in industry remains limited.
Our work aims to facilitate industrial adoption by developing
a toolchain that improves the usability and accessibility
of MPST for industry use. This effort is guided by examples
from Paxos — a fault-tolerant consensus algorithm
known for its complexity, stemming from intricate message
exchanges that are both challenging to understand and
implement correctly.
</p>
<p>
In this talk, we extend previous work that models
crash-stop processes and failure recovery via crash branches.
Specifically, we present different ways and their challenges
to semi-automatic refactoring of global protocols
to facilitate crash branches introduction. Additionally,
we introduce a fine-grained method to simulate crashed links
using default communications, helping to prolong the session's
lifespan. Finally, we extend both the Scribble language and
Effpi, an MPST-based concurrency library for Scala,
with syntactic sugar to enhance the modularity of MPST.
</p>
</div>
</td>
</tr>
</table>
<h4>15:30 — 16:00 COFFEE</h4>
<h4>16:00 — 17:00 SESSION 3</h4>
<table>
<tr>
<td class="author">
Paul Keir<br/>(University of the West of Scotland)
</td>
<td class="title">
<span>
ClangOz:
Parallel constant evaluation of C++ map and reduce operations
</span>
<div class="abstract" id="Paul/button">
<button onclick="showAbstract('Paul')">Abstract</button>
</div>
<div class="abstract" id="Paul/abstract" style="display:none;">
<button onclick="hideAbstract('Paul')">Hide Abstract</button>
<p>
Interest in metaprogramming, reflection, and compile-time
evaluation continues to inspire and foster innovation among
the users and designers of the C++ programming language.
Regrettably, the impact on compile-times of such features
can be significant; and outside of build systems,
multi-core parallelism is unable to bring down
compilation times of individual translation units.
We present ClangOz, a novel Clang-based research compiler
that addresses this issue by evaluating annotated
constant expressions in parallel,
thereby reducing compilation times.
</p>
</div>
</td>
</tr>
<tr>
<td class="author">
Jeremy Singer<br/>(University of Glasgow)
</td>
<td class="title">
<span>
Esoteric Programming Languages and Why We Should Take Them Seriously
</span>
<div class="abstract" id="Jeremy/button">
<button onclick="showAbstract('Jeremy')">Abstract</button>
</div>
<div class="abstract" id="Jeremy/abstract" style="display:none;">
<button onclick="hideAbstract('Jeremy')">Hide Abstract</button>
<p>
Esoteric programming languages are fun to learn, and their
unusual features and constraints can improve programming ability.
From languages designed to be intentionally obtuse
(e.g. INTERCAL) to others targeting artistic expression
(e.g. Piet) or philosophical exploration (e.g. Chef),
this talk examines how esoteric languages push the boundaries
of software development.
</p>
<p>
My key thesis is that esoteric languages can improve general
PL awareness, as well as enabling the esoteric programmer to
impress their peers with obscure knowledge.
We will explore why people are attracted to esoteric languages
in terms of (a) program comprehension and coding, as well as
(b) language design and implementation.
</p>
</div>
</td>
</tr>
</table>
<h4>17:00 — late PUB</h4>
<ul>
<li><a href="https://www.themeadowparkstirling.co.uk/">The Meadowpark</a> — right next to the University campus (serves decent food, too)</li>
</ul>
</section>
<section>
<h3><a name="travel" class="anchor">Travel</a></h3>
<ul>
<li><a href="https://www.stir.ac.uk/about/getting-here/">Getting to Stirling</a> (by public transport, car, ...)</li>
<li><a href="https://www.stir.ac.uk/about/getting-here/parking/">Parking on Campus</a> (not free)
<ul>
<li>Free on-street parking is available about 20 minutes on foot from the Cottrell Building, e.g. at the top of Kenilworth Road.</li>
</ul>
</li>
</ul>
<div class="map" style="width: 800px; text-align: center;">
<iframe src="https://www.google.com/maps/embed?pb=!1m14!1m8!1m3!1d4445.46439470566!2d-3.9207219999999996!3d56.144444!3m2!1i1024!2i768!4f13.1!3m3!1m2!1s0x0%3A0xd5667ee63dcd12d7!2zNTbCsDA4JzQwLjAiTiAzwrA1NScxNC42Ilc!5e0!3m2!1sen!2suk!4v1662988499795!5m2!1sen!2suk" width="800" height="450" style="border:0;" allowfullscreen="" loading="lazy" referrerpolicy="no-referrer-when-downgrade" title="Map of the Cottrell Building, Main Entrance"></iframe>
Map of the Cottrell Building
</div>
</section>
<section>
<h3><a name="organisers" class="anchor">Organisers</a></h3>
<ul>
<li>Patrick Maier <patrick DOT <i>lastname</i> AT stir DOT ac DOT uk></li>
<li>Jakub Konopka <j DOT m DOT <i>lastname</i> AT stir DOT ac DOT uk></li>
<li>Giancarlo Catalano <g DOT a DOT <i>lastname</i> AT stir DOT ac DOT uk></li>
</ul>
</section>
<footer>
<hr>
<p class="footer">
Last updated: 22 February 2025
</p>
</footer>
</body>
</html>