-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy pathindex.html
More file actions
411 lines (366 loc) · 20.3 KB
/
index.html
File metadata and controls
411 lines (366 loc) · 20.3 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
<!DOCTYPE HTML>
<!--
Editorial by HTML5 UP
html5up.net | @ajlkn
Free for personal and commercial use under the CCA 3.0 license (html5up.net/license)
-->
<html>
<head>
<title>SPLS</title>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1, user-scalable=no" />
<link rel="stylesheet" href="assets/css/main.css" />
</head>
<body class="is-preload">
<!-- Wrapper -->
<div id="wrapper">
<!-- Main -->
<div id="main">
<div class="inner">
<!-- Header -->
<header id="header">
<a href="index.html" class="logo">The 20<sup>th</sup> anniversary edition of <strong>SPLS</strong> • 6<sup>th</sup>
November 2024</a>
</header>
<!-- Banner -->
<section id="banner">
<div class="content">
<header>
<h1>SPLS</h1>
<p>The Scottish Programming Languages Seminar</p>
</header>
<p>
The SPLS series is an informal meeting of the <a href="https://spli.scot">Scottish Programming Languages Institute (SPLI)</a> Community for discussing anything related to programming languages.</br></br>
This edition (the 20th anniversary edition of SPLS!) will be held and organised by the the School of Computing Science at the <strong>University of Glasgow</strong> on the <strong>6th November 2024</strong>.
The seminar will be held as a hybrid event, supporting both in-person and remote participation.
</p>
<p>
<!-- If you plan to attend in person, please register by <strong>Friday, 25<sup>th</sup> October 2024</strong> so that we have numbers for catering. -->
In-person registration is now closed.
No registration is required for remote participants.
</p>
<!-- <p>If you would like to propose a talk, please email <a href="mailto:glasgow-spls-organisers@lists.cent.gla.ac.uk">the organisers</a> with a tentative talk title.</p> -->
<!-- <ul class="actions">
<li><a href="https://doodle.com/sign-up-sheet/participate/c58925c7-5bf8-433e-8d1d-9218ab900f68/select" class="button primary big">Register</a></li>
</ul> -->
</div>
<span class="image object">
<img src="images/uofg.jpg" alt="" />
</span>
</section>
<div class="box alt">
<div class="row gtr-50 gtr-uniform">
<div class="col-1"></div>
<div class="col-4"><span class="image fit"><img src="images/uofg_logo.png" alt="" /></span></div>
<div class="col-1"></div>
<div class="col-4"><span class="image fit"><img src="images/sicsa.jpg" alt="" /></span></div>
<div class="col-1"></div>
</div>
</div>
<!-- Section -->
<!-- Commenting for now
<section>
<header class="major">
<h2>How it all started</h2>
</header>
<p>
A short history of how it started
</p>
<hr class="major" />
<div class="features">
<article>
<img class="profile" src="images/phil.jpg" />
<div class="content">
<h3>Phil Wadler</h3>
<p>
Aenean ornare velit lacus, ac varius enim lorem ullamcorper dolore. Proin aliquam facilisis ante
interdum. Sed nulla amet lorem feugiat tempus aliquam.
</p>
</div>
</article>
<article>
<img class="profile" src="images/simon.jpg" />
<div class="content">
<h3>Simon Gay</h3>
<p>Aenean ornare velit lacus, ac varius enim lorem ullamcorper dolore. Proin aliquam facilisis ante
interdum. Sed nulla amet lorem feugiat tempus aliquam.</p>
</div>
</article>
</div>
</section>
-->
<!-- Section -->
<section>
<header class="major">
<h2>Programme</h2>
</header>
<h2>Keynote speaker</h2>
<p>
<img class="profile left" alt="Picture of Philip Wadler" src="images/phil.jpg" />
Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh and Senior Research Fellow at IOHK.
He is a Fellow of the Royal Society, a Fellow of the Royal Society of Edinburgh, and an ACM Fellow.
He is head of the steering committee for Proceedings of the ACM, past editor-in-chief of PACMPL and JFP, past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, winner of the SIGPLAN Distinguished Service Award, and a winner of the POPL Most Influential Paper Award.
</p>
<p>
Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris.
He has an h-index of over 70 with more than 25,000 citations to his work, according to Google Scholar.
He contributed to the designs of Haskell, Java, and XQuery, and is co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004), Generics and Collections in Java (O'Reilly, 2006), and Programming Language Foundations in Agda (2018).
He has delivered invited talks in locations ranging from Aizu to Zurich.
</p>
<hr class="major" />
<h2>Schedule</h2>
<!-- <p>The schedule will be posted here once finalised.</p> -->
<div class="table-wrapper">
<table>
<tbody>
<tr>
<th>12:00</th>
<td class="major"> <span class="icon solid fa-hamburger"></span> Lunch with coffee</td>
</tr>
<tr>
<th>12:45</th>
<td class="major">Session 1</td>
</tr>
<tr>
<td>12:45 - 13:45</td>
<td><span class="icon solid fa-chalkboard-teacher"></span> <a href="#phil_wadler">Substitution without Copy and Paste</a> • Phil Wadler</td>
</tr>
<tr></tr>
<td>13:45 - 14:15</td>
<td><a href="#james_chapman">Applying Formal Methods to Cardano</a> • James Chapman</td>
</tr>
<tr>
<th>14:15</th>
<td class="major"> <span class="icon solid fa-mug-hot"></span> Short coffee break</td>
</tr>
<tr>
<th>14:30</th>
<td class="major">Session 2</td>
</tr>
<tr>
<td>14:30 - 15:00</td>
<td><a href="#greg_brown">Freely Extending Interpreters</a> • Greg Brown</td>
</tr>
<tr>
<td>15:00 - 15:30</td>
<td><a href="#craig_ramsay">Hardware Architectures for Lazy Functional Programming, Revisited</a> • Craig Ramsay</td>
</tr>
<tr>
<td>15:30 - 16:00</td>
<td><a href="#wen_kokke">Forwarders Should Be Lazy</a> • Wen Kokke</td>
</tr>
<tr>
<th>16:00</th>
<td class="major"> <span class="icon solid fa-mug-hot"></span> Long coffee break</td>
</tr>
<tr>
<th>16:30</th>
<td class="major">Session 3</td>
</tr>
<tr>
<td>16:30 - 17:00</td>
<td><a href="#jan_van_brugge">Strong Rule Induction for Syntax with Bindings</a> • Jan van Brügge</td>
</tr>
<tr>
<td>17:00 - 17:30</td>
<td><a href="#wim_vanderbauwhede">A Tale of Two Compilers</a> • Wim Vanderbauwhede</td>
</tr>
</tbody>
<tfoot>
<tr>
<th>17:30 - late</th>
<td class="major"><span class="icon solid fa-glass-cheers"></span> Pub and dinner</td>
</tr>
</tfoot>
</table>
</div>
<hr class="major" />
<h2>Post-seminar social gathering</h2>
<p>
<!-- We will organise informal drinks in a nearby pub for after the seminar, and will book a group dinner for afterwards. Details will appear here closer to the time. -->
We have dinner booked at <strong>Mosob Ethiopian & Eritrean Restaurant</strong>, 56 Dundas Street, Glasgow G1 2AQ.
The reservation is at 18:30, which gives attendees ample time to reach the dinner venue.
We can take the subway from Hillhead station to Buchanan Street station.
Mosob is in the City Centre, next to Queen Street station and close to Glasgow Central train station.
</p>
<p>
We may visit the pub afterwards.
</p>
</section>
<section>
<header class="major">
<h2>Abstracts</h2>
</header>
<p>
You can find the abstracts and a downloadable version of the slides provided by speakers.
Slides will be uploaded after the event.
</p>
<hr class="major" />
<ol>
<li>
<p>
<a name="phil_wadler">Substitution without Copy and Paste</a> • <strong>Phil Wadler</strong> • University of Edinburgh
<a href="slides/phil-wadler.pdf" class="button small icon solid fa-download download">Slides</a>
</p>
<p>
The definition of substitution in the presence of lambda binding is notoriously difficult to get correct.
The best technique, which I first learned from Conor McBride, is straightforward but does everything twice, defining renaming first and substitution second.
That is not so bad, but the key result describing composition explodes into four proofs, with either renaming or substitution on both the left and right.
This talk describes a new approach that collapses the two definitions to one definition and the four proofs to one proof.
The result includes a set of rewrites (taken from Autosubst) that can simplify any equation involving substitution.
Our work is available as an Agda script.
</p>
<p>
This is joint work with Thorsten Altenkirch and Nathaniel Burke.
</p>
</li>
<li>
<p>
<a name="james_chapman">Applying Formal Methods to Cardano</a> • <strong>James Chapman</strong> • IOHK Research
<!-- <a href="#" class="button small icon solid fa-download download">Slides</a> -->
</p>
<p>
Cardano is a Proof-of-Stake cryptocurrency with a market cap in the tens of billions of USD and a daily volume of hundreds of millions of USD.
In this paper we reflect on applying formal methods, functional architecture and Haskell to building Cardano.
We describe our strategy, our projects, reflect on lessons learned, the challenges we face and how we propose to meet them.
</p>
</li>
<li>
<p>
<a name="greg_brown">Freely Extending Interpreters</a> • <strong>Greg Brown</strong> • University of Edinburgh
<a href="slides/greg-brown.pdf" class="button small icon solid fa-download download">Slides</a>
</p>
<p>
A partial evaluator extends an interpreter to work on terms with free variables.
In this talk, I will formalise this intuition for pure simply-typed languages.
I will focus on the simply-typed lambda calculus, but my definitions are in terms of any second-order algebra as defined by Fiore.
After giving a definition for a denotational interpreter, I will define what it means for a model of a language (formulated as a SOAS algebra) to extend an interpreter, as well as morphisms between extensions.
From this, I will define the free extension of an interpreter, which is the least opinionated partial evaluator.
</p>
<p>
This is work in progress towards my PhD.
</p>
</li>
<li>
<p>
<a name="craig_ramsay">Hardware Architectures for Lazy Functional Programming, Revisited</a> • <strong>Craig Ramsay</strong> • Heriot-Watt University
<a href="slides/craig-ramsay.pdf" class="button small icon solid fa-download download">Slides</a>
</p>
<p>
Custom hardware architectures for functional languages enjoyed a boom in the 80s and 90s following Backus' Turing Award lecture "Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs".
Research interest later waned due to difficulties in matching the rapid pace of RISC processor development and compiler techniques.
</p>
<p>
This talk from the HAFLANG project re-explores these ideas in a modern landscape --- where single-thread performance of stock CPUs have begun to stagnate, but the performance of hardware prototyping platforms such as FPGAs have not.
We present the Heron processor for evaluating non-strict functional programs, as well as its concurrent hardware garbage collector.
While still slightly slower than conventional platforms, it offers interesting advantages in energy efficiency and opportunity for formal verification from source language down to hardware implementation.
We also propose a path towards a single-chip many-core architecture.
</p>
</li>
<li>
<p>
<a name="wen_kokke">Forwarders Should Be Lazy</a> • <strong>Wen Kokke</strong> • Strathclyde University and the University of Edinburgh
<a href="slides/wen-kokke.pdf" class="button small icon solid fa-download download">Slides</a>
</p>
<p>
Classical Processes is a process calculus interpretation of Classical Linear Logic.
Nominally, CP interprets CLL's axiom as a <em>forwarder</em> process, which sends any message it receives over its input channel over its output channel.
Operationally, CP's forwarders do not forward messages at all.
Instead, they put their input and output channels together and terminate.
This causes lots of trouble with CP's metatheory and its use as a model of concurrent computation.
</p>
<p>
I propose an alternative operational semantics for forwarders which avoids this trouble and has an pleasant interpretation in CLL.
</p>
</li>
<li>
<p>
<a name="jan_van_brugge">Strong Rule Induction for Syntax with Bindings</a> • <strong>Jan van Brügge</strong> • Heriot-Watt University
<a href="slides/jan-van-brugge.pdf" class="button small icon solid fa-download download">Slides</a>
</p>
<p>
When reasoning about inductively defined predicates over syntax with bindings, keeping bound variables fresh helps to reduce the complexity of the proofs.
We have identified a general criteria when it is possible to strengthen the induction theorem derived from the knaster-tarski fixpoint underlying the inductive predicate to avoid bound variables.
This criteria is not dependent on the syntactic format of the rules, and thus supports e.g. higher order relators and quantifiers in the predicate without requiring extra side conditions.
</p>
</li>
<li>
<p>
<a name="wim_vanderbauwhede">A Tale of Two Compilers</a> • <strong>Wim Vanderbauwhede</strong> • University of Glasgow
<a href="slides/wim-vanderbauwhede.pdf" class="button small icon solid fa-download download">Slides</a>
</p>
<p>
This talk is about a side project I did on compiling Fortran to Uxn, a tiny stack-based VM with 64 kB memory and 8-bit instructions.
The talk focuses on two languages: Fortran (naturally) and Funktal, a strict, statically typed functional language for Uxn; and on their compilers: a general purpose, "serious" source-to-source compiler for Fortran, and a custom, "frivolous" compiler from Funktal.
The link between the two will become clear in the talk.
</p>
</li>
</ol>
</section>
</div>
</div>
<!-- Sidebar -->
<div id="sidebar">
<div class="inner">
<!-- Menu -->
<!-- Section -->
<section>
<header class="major">
<h2>Getting here</h2>
</header>
<p>
<article>
<iframe
src="https://www.google.com/maps/embed?pb=!1m18!1m12!1m3!1d2279.1529661412287!2d-4.294432123064445!3d55.87394807312937!2m3!1f0!2f0!3f0!3m2!1i1024!2i768!4f13.1!3m3!1m2!1s0x488845ce6c50ce15%3A0x9891fb78c4c05809!2sSir%20Alwyn%20Williams%20Building%2C%20Glasgow%20G12%208QN!5e1!3m2!1sen!2suk!4v1724836260988!5m2!1sen!2suk"
width="272" height="204" style="border:0;" allowfullscreen="" loading="lazy"
referrerpolicy="no-referrer-when-downgrade"></iframe>
</article>
</p>
<ul class="contact">
<li class="icon solid fa-map-pin">
<strong>Room 422 • 423</strong><br>
School of Computing Science<br>
Sir Alwyn Williams Building<br>
University of Glasgow, G12 8RZ
</li>
</ul>
<p>The easiest way to reach the School of Computing Science is by taking the Glasgow Subway to Hillhead.
The closest subway station to Glasgow Queen Street station is <em>Buchanan Street</em>, and the closest subway station to Glasgow Central is <em>St Enoch</em>.
Rooms will be signposted on the day.</p>
</section>
<!-- Section -->
<section>
<header class="major">
<h2>Organising committee</h2>
</header>
<ul class="contact">
<li class="icon solid fa-envelope">
Should you have comments or queries about the event, please contact one of the organisers by <a href="mailto:glasgow-spls-organisers@lists.cent.gla.ac.uk">email</a> or on
Zulip. This edition of SPLS is organised by:
</li>
</ul>
</p>
<ul class="contact">
<li>
<p>Simon Fowler</p>
<p>Jeremy Singer</p>
<p>Olivia Weston</p>
<p>Duncan Paul Attard</p>
</li>
</ul>
</section>
<!-- Footer -->
<footer id="footer">
<p class="copyright">© Scottish Programming Languages Institute. Design adapted from <a href="https://html5up.net">HTML5 UP</a>.</p>
</footer>
</div>
</div>
</div>
<!-- Scripts -->
<script src="assets/js/jquery.min.js"></script>
<script src="assets/js/browser.min.js"></script>
<script src="assets/js/breakpoints.min.js"></script>
<script src="assets/js/util.js"></script>
<script src="assets/js/main.js"></script>
</body>
</html>