-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy pathindex.html
More file actions
439 lines (407 loc) · 15.6 KB
/
index.html
File metadata and controls
439 lines (407 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
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8"/>
<meta name="viewport" content="width=device-width,initial-scale=1"/>
<title>SPLS, 26 October 2022, 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, 26th October 2022</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>Cottrell Building, room 2A73</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="../../2019/june/static/images/sicsa_blue.jpg" alt="SICSA Logo"></a>
<a href="https://www.stir.ac.uk/"><img class="logo" src="../../2020/march/uos-logo.svg" alt="University of Stirling Logo" style="height:48px;"></a>
</div>
</header>
<section>
<h3><a name="programme" class="anchor">Programme</a></h3>
<h4>09:30 — 12:00 PhD EVENT</h4>
<table>
<tr>
<td class="phdevent">
In-person event for PhD students, organised by the <a href="https://scottish-pl-institute.github.io/">SPLI</a>.
<ul>
<li>09:30 — 10:00 Breakfast & welcome</li>
<li>10:00 — 11:00 University & SPLI presentation </li>
<li>11:30 — 12:00 Live Q&A; you can send in your questions anonymously <a href=https://hackmd.io/@wgYOT8jJR7C7aXnw2gzP2A/BJ_iR9pGj/edit>here</a>.
</ul>
</td>
</tr>
</table>
<h4>12:00 — 13:00 LUNCH</h4>
<h4>13:00 — 14:00 SESSION 1: Program Transformations</h4>
<table>
<tr>
<td class="author">
Anton Lorenzen (Edinburgh)
</td>
<td class="title">
<span>
Balanced Search Tree Insertion:
Functional is Top-down is Bottom-up
</span>
<div class="abstract" id="Anton/button">
<button onclick="showAbstract('Anton')">Abstract</button>
</div>
<div class="abstract" id="Anton/abstract" style="display:none;">
<button onclick="hideAbstract('Anton')">Hide Abstract</button>
<p>
For splay trees, zip trees and red-black trees there are
versions of the insertion function: A functional one
that balances after a recursive call, a top-down
imperative one that balances on the way down and a
bottom-up imperative one that balances on the way up. In
this work, we aim to show that these superficially
different versions can be transformed into each other,
thus proving that they not only satisfy the same
invariants but actually produce the same trees. To do
this, we use compilation techniques such as reuse
analysis, the defunctionalized CPS transformation and
tail recursion modulo cons to compile the functional
implementation in two different ways, leading to the two
imperative versions.
</p>
</div>
</td>
</tr>
<tr>
<td class="author">
Ryan Kirkpatrick (St Andrews)
</td>
<td class="title">
<span>
Automated Thread Placement via Dynamic Binary Instrumentation
</span>
<div class="abstract" id="Ryan/button">
<button onclick="showAbstract('Ryan')">Abstract</button>
</div>
<div class="abstract" id="Ryan/abstract" style="display:none;">
<button onclick="hideAbstract('Ryan')">Hide Abstract</button>
<p>
We present COMPROF, our communication profiling tool for
shared-memory systems that requires no recompilation or
user intervention. We use dynamic binary instrumentation
to intercept memory operations and estimate inter-thread
communication overhead, deriving (and possibly
visualising) a communication graph of data-sharing
between threads. We then use this graph to map threads
to cores in order to optimise memory traffic through the
memory system. Different paths through a system’s memory
hierarchy have different latency, throughput and energy
properties, we exploit this heterogeneity to provide
automatic performance and energy improvements for
multi-threaded programs. We demonstrate this on the NAS
Parallel Benchmark (NPB) suite where, using our
technique, we are able to achieve improvements of up to
12% in the execution time and up to 10% in the energy
consumption (compared to default Linux scheduling) while
not requiring any modification or recompilation of the
application code.
</p>
</div>
</td>
</tr>
</table>
<h4>14:00 — 14:30 COFFEE</h4>
<h4>14:30 — 15:30 SESSION 2: Semantics</h4>
<table>
<tr>
<td class="author">
Jacques Carette (McMaster)
</td>
<td class="title">
<span>
Definite Folds
</span>
<div class="abstract" id="Jacques/button">
<button onclick="showAbstract('Jacques')">Abstract</button>
</div>
<div class="abstract" id="Jacques/abstract" style="display:none;">
<button onclick="hideAbstract('Jacques')">Hide Abstract</button>
<p>
Notions of derivative abound in functional
programming. An obvious question arises: what about
integrals? It turns out that folds are the analogous
concept. Pursuing the analogy leads us to a proper
notion of "definite fold" corresponding to definite
integrals (and sums and products and ...). Many concepts
are needed along the way (Route, Pointed type, etc). In
return, incremental and parallel versions of fold arise
naturally. The correct notion of indefinite fold is a
little more elusive, making a "Fundamental Theorem of
Fold-Calculus" delicate; two such candidates will be
presented.
</p>
<p>
This is joint work with my Ph.D. student, Noel Brett.
</p>
</div>
</td>
</tr>
<tr>
<td class="author">
Sam Lindley (Edinburgh)
</td>
<td class="title">
<span>
Encoding Product Types
</span>
<div class="abstract" id="Sam/button">
<button onclick="showAbstract('Sam')">Abstract</button>
</div>
<div class="abstract" id="Sam/abstract" style="display:none;">
<button onclick="hideAbstract('Sam')">Hide Abstract</button>
<p>
Can product types be encoded in simply-typed lambda
calculus with base types and function types? I'll show
that the answer to this apparently simple question is
more nuanced than we might expect.
</p>
</div>
</td>
</tr>
</table>
<h4>15:30 — 16:00 COFFEE</h4>
<h4>16:00 — 17:00 SESSION 3: Behavioural Types</h4>
<table>
<tr>
<td class="author">
Katarzyna Marek (Edinburgh)
</td>
<td class="title">
<span>
A Sound and Complete View-based Regex Parser
</span>
<div class="abstract" id="Katarzyna/button">
<button onclick="showAbstract('Katarzyna')">Abstract</button>
</div>
<div class="abstract" id="Katarzyna/abstract" style="display:none;">
<button onclick="hideAbstract('Katarzyna')">Hide Abstract</button>
<p>
In this talk, we present a formalization of a verified
(sound and complete) regex parser in the Idris 2
programming language. Soundness says that if the result
of parsing some text is a parse tree: 1. it is a valid
parse tree for the regex, 2. its flattening (fringe) is
a prefix of the parsed text; and completeness means,
that if parsing returns an error, there exists no parse
tree satisfying conditions (1) and (2). In our
implementation, we make use of McBride-McKinna views to
ease the proofs and get a correct parser by virtue of
its type.
</p>
<p>
This is joint work with Ohad Kammar and James McKinna.
</p>
</div>
</td>
</tr>
<tr>
<td class="author">
Simon Fowler (Glasgow)
</td>
<td class="title">
<span>
Special Delivery: Programming with Mailbox Types
</span>
<div class="abstract" id="Simon/button">
<button onclick="showAbstract('Simon')">Abstract</button>
</div>
<div class="abstract" id="Simon/abstract" style="display:none;">
<button onclick="hideAbstract('Simon')">Hide Abstract</button>
<p>
Actor-based languages such as Erlang and Elixir are
well-suited to distributed programming due to the
concept of a <em>mailbox</em>: a message queue local to each
thread of execution. However, actor languages are
vulnerable to subtle yet insidious programmer errors
such as protocol violations and communication
mismatches, which can be difficult to locate and fix.
</p>
<p>
Mailbox types, proposed by de'Liguoro and Padovani in
2018, are a behavioural type system which captures the
contents of a mailbox using a commutative regular
expression, and can rule out common communication errors
such as protocol violations, payload mismatches, and
some deadlocks. In this work, we present the first
theoretical and practical integration of mailbox types
into a programming language. Unlike session type
systems, the many-writer, single-reader nature of
mailboxes poses nontrivial challenges for language
integration. We address these challenges through the use
of Kobayashi's notion of quasi-linearity, and develop a
co-contextual algorithmic type system based on backwards
bidirectional typing.
</p>
<p>
(joint work with Simon Gay, Phil Trinder, and Franciszek Sowul)
</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</li>
</ul>
</section>
<section>
<h3><a name="attending" class="anchor">Attending</a></h3>
<h4>Registration</h4>
<ul>
<li>Please register <em>by 20th October</em> on the <a href="https://doodle.com/meeting/organize/id/e1r30j3a">SPLS Doodle poll</a> if you plan to attend SPLS in person.</li>
<li>Please register <em>by 20th October</em> on the <a href="https://doodle.com/meeting/organize/id/eE9Wgrge">PhD event Doodle poll</a> if you plan to attend the PhD event.</li>
<li>Registration is required for catering. There are no COVID restrictions on attendance. Mask wearing in packed indoor areas is encouraged, as is testing before attending.</li>
</ul>
<h4>Travel</h4>
<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/d/embed?mid=18bO5PeaxiJTGp5u0zQa8uYo4zAB0f5Q&ehbc=2E312F" width="800" height="300"></iframe>
-->
<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>
SPLS meeting:
<a href="http://www.cs.stir.ac.uk/~cpm/">Patrick Maier</a>
(email: firstname.lastname@stir.ac.uk) and
Giancarlo Catalano
</li>
<li>
PhD event:
André Videla (email: firstname.lastname@strath.ac.uk)
</li>
</ul>
</section>
<footer>
<hr>
<p class="footer">
Last updated: 18 October 2022
</p>
</footer>
</body>
</html>