-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathindex.html
451 lines (388 loc) · 15.6 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
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
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8"/>
<meta name="viewport" content="width=device-width,initial-scale=1"/>
<title>SPLS, 07 June 2023, University of the West of Scotland</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, 7th June 2023</h2>
<p>
The <a href="../../../">Scottish Programming Languages Seminar (SPLS)</a>
is an informal meeting for discussing anything related to
programming languages.
</p>
<p>
This edition of SPLS will be held both <strong>in-person</strong>
and <strong>online</strong>.
The in-person meeting will take place in the
<strong>Coats Building, room P118</strong>
at the <strong>University of the West of Scotland</strong>.
</p>
<p>
This edition of SPLS is sponsored by <a href="https://www.sicsa.ac.uk/">SICSA</a> (Theory, Modelling & Computation Research Theme).
</p>
<div class="header">
<a href="https://www.sicsa.ac.uk/"><img class="logo" src="../../2019/june/static/images/sicsa_blue.jpg" alt="SICSA Logo"></a>
<a href="https://www.uws.ac.uk">
<img class="logo" src="./uws-logo-black-resized.png" alt="University of the West of Scotland">
</a>
</div>
</header>
<section>
<h3><a name="programme" class="anchor">Programme</a></h3>
<h4>12:00 — 13:00 LUNCH</h4>
<h4>13:00 — 14:00 SESSION 1: Invited Talk</h4>
<table>
<tr>
<td class="author">
Matija Pretnar (Ljubljana)
</td>
<td class="title">
<span>
Asynchronous Effects
</span>
<div class="abstract" id="Matija/button">
<button onclick="showAbstract('Matija')">Abstract</button>
</div>
<div class="abstract" id="Matija/abstract" style="display:none;">
<button onclick="hideAbstract('Matija')">Hide Abstract</button>
<p>
In the standard algebraic approach to effects, once an operation
is called, the evaluation of the continuation stalls until it gets a result
(either from a built-in primitive effect or through a handler). But we often
desire asynchronous behaviour, when the continuation may proceed with the
evaluation and suitably incorporates the result once it arrives. I will
describe a small calculus with primitives for sending such signals and
receiving corresponding interrupts, and show a small prototype in which one can
express promises, preemptive multi-threading and remote function calls.
</p>
<p>
Joint work with Danel Ahman.
</p>
</div>
</td>
</tr>
</table>
<h4>14:00 — 14:30 COFFEE</h4>
<h4>14:30 — 16:00 SESSION 2: Logic</h4>
<table>
<tr>
<td class="author">
Murdoch Gabbay (Heriot-Watt)
</td>
<td class="title">
<span>
Semitopology: a new topological model of heterogeneous consensus
</span>
<div class="abstract" id="Murdoch/button">
<button onclick="showAbstract('Murdoch')">Abstract</button>
</div>
<div class="abstract" id="Murdoch/abstract" style="display:none;">
<button onclick="hideAbstract('Murdoch')">Hide Abstract</button>
<p>
A distributed system is permissionless when participants can join and leave the
network without permission from a central authority. Many modern distributed
systems are naturally permissionless, in the sense that a central permissioning
authority would defeat their design purpose: this includes blockchains,
filesharing protocols, some voting systems, and more. By their permissionless
nature, such systems are heterogeneous: participants may only have a partial
view of the system, and they may also have different goals and beliefs. Thus,
the traditional notion of consensus -- i.e. system-wide agreement -- may not be
adequate, and we may need to generalise it.
</p>
<p>
This is a challenge: how should we understand what heterogeneous consensus is;
what mathematical framework might this require; and how can we use this to
build understanding and mathematical models of robust, effective, and secure
permissionless systems in practice?
</p>
<p>
We analyse heterogeneous consensus using semitopology as a framework. This is
like topology, but without the restriction that intersections of opens be open.
Semitopologies have a rich theory which is related to topology, but with its
own distinct character and mathematics. We introduce novel well-behavedness
conditions, including an anti-Hausdorff property and a new notion of `topen
set', and we show how these structures relate to consensus. We give a
restriction of semitopologies to witness semitopologies, which are an
algorithmically tractable subclass corresponding to Horn clause theories,
having particularly good mathematical properties. We introduce and study
several other basic notions that are specific and novel to semitopologies, and
study how known quantities in topology, such as dense subsets and closures,
display interesting and useful new behaviour in this new semitopological
context.
</p>
</div>
</td>
</tr>
<tr>
<td class="author">
Xueying Qin (Edinburgh)
</td>
<td class="title">
<span>
Shoggoth - A Formalised Logic for Strategic Rewriting
</span>
<div class="abstract" id="Xueying/button">
<button onclick="showAbstract('Xueying')">Abstract</button>
</div>
<div class="abstract" id="Xueying/abstract" style="display:none;">
<button onclick="hideAbstract('Xueying')">Hide Abstract</button>
<p>
Strategic rewriting languages provide programmers with combinators and generic
traversals that allow them to compose rewrite rules and control their
application. Strategic rewriting has applications in many domains, including
interpreter/compiler for DSLs (Spoofax/Stratego) and program optimisation
(ELEVATE). It is important to reason about strategies, to ensure that they are
well-composed (do not result in error), do not diverge and indeed rewrites
expressions into forms that satisfy desired properties. To formally understand
strategies, we formalise a denotational semantics of the strategy rewriting
language System S and demonstrates its correspondence to existing big-step
operational semantics. To facilitate formal reasoning over strategies, we
formalise the weakest precondition calculus for System S, and demonstrate that
it can be used to reason about whether or not a strategy terminates and is
well-composed as well as the execution of a strategy leads to the result that
satisfies desired properties.
</p>
</div>
</td>
</tr>
<tr>
<td class="author">
Fredrik Nordvall Forsberg (Strathclyde)
</td>
<td class="title">
<span>
Set theory or type theory? It doesn't matter! (For ordinals)
</span>
<div class="abstract" id="Fredrik/button">
<button onclick="showAbstract('Fredrik')">Abstract</button>
</div>
<div class="abstract" id="Fredrik/abstract" style="display:none;">
<button onclick="hideAbstract('Fredrik')">Hide Abstract</button>
<p>
Ordinals are useful for justifying termination, and giving semantics to
inductive definitions, but should one use set theory or type theory to develop
the theory of ordinals? In constructive set theory, an ordinal is usually
understood as a hereditarily transitive set, whereas in homotopy type theory,
an ordinal is a type with a transitive, wellfounded, and extensional binary
relation -- two seemingly quite different approaches! However, we show that
they are actually the same, in the following sense: working in homotopy type
theory, we can use (a higher-inductive refinement of) Aczel's interpretation of
constructive set theory into type theory to construct a type of set-theoretic
ordinals. We show that this type is equal to the type of type-theoretic
ordinals. Going further, we also show how the notion of a type-theoretic
ordinal can be generalised to a natural class of ordered structures, which
captures all sets in Aczel's interpretation.
</p>
<p>
This is joint work with Tom de Jong, Nicolai Kraus and Chuangjie Xu, and
will appear at LICS this year.
</p>
<p>
Preprint:
<a href="https://arxiv.org/abs/2301.10696"> https://arxiv.org/abs/2301.10696</a>
<p>
</div>
</td>
</tr>
</table>
<h4>16:00 — 16:30 COFFEE</h4>
<h4>16:30 — 17:30 SESSION 3: Semantics and Security</h4>
<table>
<tr>
<td class="author">
Filip Sieczkowski (Heriot-Watt)
</td>
<td class="title">
<span>
Call-by-value and call-by-name: it's elementary!
</span>
<div class="abstract" id="Filip/button">
<button onclick="showAbstract('Filip')">Abstract</button>
</div>
<div class="abstract" id="Filip/abstract" style="display:none;">
<button onclick="hideAbstract('Filip')">Hide Abstract</button>
<p>
To any functional programmer, it is intuitively obvious that call-by-name
evaluation can simulate the call-by-value one. However, most proofs of this
fact are rather complex, or follow as corollaries from significantly more
involved theorems. In this talk I will demonstrate a simple approach to proving
this simulation result, with some methodological takeaways.
</p>
</div>
</td>
</tr>
<tr>
<td class="author">
Jeremy Singer and Dejice Jacob (Glasgow)
</td>
<td class="title">
<span>
Picking a CHERI Allocator: Security and Performance Considerations
</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>
Several open-source memory allocators have been ported to CHERI, a hardware
capability platform. In this presentation we examine the security and
performance of these allocators when run under CheriBSD on Arm’s prototype
Morello platform. We introduce a number of security attacks and show that all
but one allocator are vulnerable to some of the attacks - including the default
CheriBSD allocator. We then show that while some forms of allocator performance
are meaningful, comparing the performance of hybrid and pure capability (i.e.
‘running in non-CHERI vs. running in CHERI modes’) allocators does not
currently appear to be meaningful. Although we do not fully understand the
reasons for this, it seems to be at least as much due to factors such as
immature compiler toolchains and prototype hardware as it is due to the effects
of capabilities on performance.
</p>
</div>
</td>
</tr>
</table>
<h4>17:30 — late PUB</h4>
<p>
We have a reservation at the Bull Inn on New Street; a short walk from the Coats Building.
</p>
</section>
<section>
<h3><a name="attending" class="anchor">Attending</a></h3>
<p>
For the online participants, we will use <a href="https://teams.microsoft.com/l/meetup-join/19%3ameeting_ZDNhOTgzMmYtMWZiNi00MmY3LWI5ODgtODMwMGE0ZDc3NWZk%40thread.v2/0?context=%7b%22Tid%22%3a%22f89944b7-4a4e-4ea7-9156-3299f3411647%22%2c%22Oid%22%3a%229ad34bb4-5d96-4fd0-aa48-d74f90bbd60f%22%7d">This Teams Meeting Link</a>.
</p>
<h4>Registration</h4>
<ul>
<li>Please register <s><em>by 30th May</em></s> <em>by 2nd June</em> on the <a href="https://doodle.com/meeting/participate/id/az7gnEYb">SPLS Doodle poll</a> if you plan to attend SPLS in person.</li>
<li>Registration is required for catering. There are no COVID restrictions on attendance. Mask wearing in packed indoor areas is welcomed, as is testing before attending.</li>
</ul>
<h4>Travel</h4>
<ul>
<li>By train from Glasgow Central to <a href="https://www.scotrail.co.uk/plan-your-journey/stations-and-facilities/pyg">Paisley Gilmour Street</a> and a 10 minute walk via High Street.
</li>
<li>Glasgow Central Train Station is a 10 minute walk from Glasgow Queen Street Train Station.
</li>
<li>Car parking is available at the nearby <a href="https://www.openstreetmap.org/?mlat=55.84393&mlon=-4.42709#map=18/55.84393/-4.42709">Paisley Centre Car Park</a>.
</li>
<li>Further travel info from the University is <a href="https://www.uws.ac.uk/university-life/campuses/paisley-campus/travelling-to-paisley-campus">here</a>; and a pdf campus map is <a href="https://www.uws.ac.uk/media/6469/paisley-campus-welcome-map.pdf">here</a>.
<li>The Coats Building on the map (<a href="https://www.openstreetmap.org/?mlat=55.84391&mlon=-4.42868#map=17/55.84391/-4.42868">larger version</a>):
</li>
</ul>
</section>
<section>
<div class="map" style="width: 800px; text-align: center;">
<iframe width="800" height="400" frameborder="0" scrolling="no" marginheight="0" marginwidth="0" src="https://www.openstreetmap.org/export/embed.html?bbox=-4.43274753373755%2C55.842166041222356%2C-4.424609711586365%2C55.84565075073519&layer=mapnik&marker=55.843906929574345%2C-4.428676110146284" style="border: 1px solid black"></iframe>
</div>
</section>
<section>
<h3><a name="organisers" class="anchor">Organisers</a></h3>
<p>Paul Keir and Santiago Matalonga <firstname DOT lastname AT uws DOT ac DOT uk></p>
</section>
<footer>
<hr>
<p class="footer">
Last updated: 8th June 2023
</p>
</footer>
</body>
</html>