-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathindex.html
427 lines (378 loc) · 16.1 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
<!DOCTYPE html>
<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/sakura.css/css/sakura.css" type="text/css">
<title>SPLS 6th March 2024, University of St Andrews</title>
<style>
/* TODO: is this styling actually needed?
.column {
float: right;
width: 30%;
padding: 15px;
}
.row {
margin-top: 26px;
display: block;
margin-left: auto;
margin-right: auto;
width: 100%;
padding-bottom: 0px;
/*border: 1px solid black;
}
/* Clearfix (clear floats)
.row::after {
content: "";
clear: both;
display: table;
}
*/
/* Some custom styling for certain elements */
.time {
vertical-align: top;
}
/* grey background for breaks */
.break {
background: #E6E6E6;
}
.talk-title {
text-decoration: underline;
}
.talk-abstract {
display: none;
}
td, th {
vertical-align: top;
}
</style>
<script>
function toggleAbstract(id) {
var e = document.getElementById(id);
s = getComputedStyle(e, null).display;
if (s === "none") {
e.style.display = "block";
} else {
e.style.display = "none";
}
}
</script>
</head>
<body>
<header>
<h1>SPLS — 6th March 2024 (12:00–17:30)</h1>
<div class="row">
<div class="column">
<a href="https://www.st-andrews.ac.uk/">
<img src="/spls/assets/images/st-andrews.png" alt="University of St Andrews logo">
</a>
</div>
<div class="column">
<a href="https://www.sicsa.ac.uk/">
<img src="/spls/assets/images/sicsalogo.png" alt="SICSA logo">
</a>
<p>
We acknowledge and are grateful for the continued sponsorship of SPLS by
the
<a href="https://www.sicsa.ac.uk/">
Scottish Informatics and Computer Science Alliance (SICSA)
</a>
</p>
</div>
</div>
</header>
<section>
<h2>Attendance</h2>
<p>
The talks will be held on the North Haugh, in the Willie Russell Building,
lecture theatre C.
</p>
<details>
<summary>Audio-Visual (AV) equipment details</summary>
(This is mostly of relevance to the presenters.)
<ul>
<li>
General overview
<img src="assets/av-setup-pictures/wrlc-overview.jpg"
alt="Picture overview of the theatre: a whiteboard to the left, 3
large TVs in the middle, and a computer with a document
camera on the right. Chairs are lined up in the
foreground.">
</li>
<li>
Adapters/Dongles from USB-C, DisplayPort, and Mini DisplayPort, each
to HDMI.
<img src="assets/av-setup-pictures/wrlc-display-adapters.jpg"
alt="Picture of the male side of 3 display adapters">
</li>
<li>
Document camera
<img src="assets/av-setup-pictures/wrlc-document-camera.jpg"
alt="Picture of a document camera">
</li>
<li>
Rolling whiteboard
<img src="assets/av-setup-pictures/wrlc-rolling-whiteboard.jpg"
alt="Picture of a rolling whiteboard in a frame on wheels">
</li>
</ul>
<h3>Platforms</h3>
<p>
There is a channel, <i>#spls-2024-03</i>, set up on the
<a href="https://spls.zulipchat.com/">SPLS Zulip</a> chat service.
</p>
</section>
<section>
<h3>Programme</h3>
All the times below are given in Greenwich Mean Time (GMT), i.e. UTC+0.
<table style="text-align: left">
<tr>
<th>Time</th>
<th>Speaker</th>
<th>Title</th>
</tr>
<tr class="break">
<td> 12:00 – 12:45 </td>
<td colspan=2> Lunch </td>
</tr>
<tr>
<td class="time"> 12:45 – 13:15 </td>
<td> Andy Gordon (Cogna Ltd and University of Edinburgh) </td>
<td>
<a class="talk-title" href="javascript:toggleAbstract('abstract0')">
Rise of the AI-Empowered End User Software Engineer
</a>
<div id="abstract0" class="talk-abstract">
<p>
What if natural language really is the new programming language?
Inspired by the transformation of professional software
engineering by generative AI, let’s take the next step: empowering
end users. We can boost their productivity with hyper-customized
software generated from natural language. This challenge needs
research right across software engineering: requirements,
architecture, coding, testing, verification, repair, and
maintenance. My talk will survey current progress and open
research questions in this exciting new area of programming
language research.
</p>
</div>
</td>
</tr>
<tr>
<td class="time"> 13:15 – 13:45 </td>
<td> Ferdia McKeogh (St Andrews) </td>
<td>
<a class="talk-title" href="javascript:toggleAbstract('abstract1')">
How to Compile a Compiler
</a>
<div id="abstract1" class="talk-abstract">
<p>
In this talk we present our work thus far on a toolchain for
compiling a model of an instruction set architecture (ISA) to a
performant dynamic binary translator (DBT) for that architecture.
An instruction set architectures (ISA) is the specification of the
interface between hardware and software in modern processors.
Emulating ISAs allows software for a given architecture to be
executed on a host machine with a different architecture. This is
useful for running, debugging, and testing such software when
hardware for the target architecture is unavailable. Sail is a
popular language for describing instruction set architectures
(ISAs). Sail models of ISAs can be compiled to produce an emulator
for that ISA. Many Sail models for popular architectures already
exist; models for Arm architectures can be produced automatically
from Arm’s internal specification, and RISC-V uses Sail for their
authoritative specification. However, the emulators produced by
the Sail compiler are relatively slow and do not take advantage of
modern emulation techniques. Faster emulators can be written
either by hand or using a different ISA description language, but
this requires the slow, labour-intensive, and error-prone process
of manually translating from the authoritative specifications into
the target language. The proposed solution is to automated this
process with a compiler that takes a Sail model as an input, and
produces a fast emulator of that architecture, drastically
reducing the time cost and improving correctness.
</p>
</div>
</td>
</tr>
<tr>
<td class="time"> 13:45 – 14:15 </td>
<td> Ellis Kesterton (St Andrews) </td>
<td>
<a class="talk-title" href="javascript:toggleAbstract('abstract2')">
Zero Cost Higher-Order Functions
</a>
<div id="abstract2" class="talk-abstract">
<p>
Higher-order functions are the key feature of most functional
languages. They enable the programmer to abstract out common
algorithmic patterns, resulting in cleaner and more modular code.
Unfortunately, higher-order programs are often less efficient than
their first-order counterparts due to the creation of closures at
run-time. This talk discusses a compile-time program
transformation which converts a higher-order program into an
equivalent first-order one, through a specialisation technique
based on partial evaluation. By adapting the work on
Normalisation-by-Evaluation, we derive an efficient, easily
verifiable algorithm for performing this transformation.
</p>
</div>
</td>
</tr>
<tr class="break">
<td> 14:15 – 14:30 </td>
<td colspan=2> Coffee break </td>
</tr>
<tr>
<td class="time"> 14:30 – 15:00 </td>
<td> Meven Lennon-Bertrand (Cambridge) </td>
<td>
<a class="talk-title" href="javascript:toggleAbstract('abstract3')">
Definitional Functoriality for Dependent (Sub)Types
</a>
<div id="abstract3" class="talk-abstract">
<p>
There are two standard approaches to subtyping. In the subsumptive
one, subtyping is implicit and does not appear in program code,
while in the coercive one each usage of subtyping has to be
explicitly marked with <em>coercions</em>. Users do not want to
put coercions in, yet they make the life of the semanticist much
easier and cleaner. One can elaborate programs from the
subsumptive to the coercive discipline, by adding coercions
wherever needed, based on a typing derivation. However, when there
are multiple derivations for the same program, these lead to
different elaborations. This is tackled by a coherence theorem,
which says that any two elaboration of the same program have the
same semantics. As usual, the story becomes more complicated with
dependent types, where the equational theory of programs appears
during typing. In other words, to show that elaboration is
type-preserving, we need coherence to hold. Yet, the equations
demanded by coherence, which correspond to a form of functoriality
of type-formers, do not hold on the nose in vanilla MLTT.
Fortunately, this is repairable: I will show how to add these
functoriality equations, while keeping all the other good
properties, allowing for a type-preserving elaboration.
</p>
</div>
</td>
</tr>
<tr>
<td class="time"> 15:00 – 15:30 </td>
<td> Thomas Hansen (St Andrews) </td>
<td>
<a class="talk-title" href="javascript:toggleAbstract('abstract4')">
Increasing confidence in Types
</a>
<div id="abstract4" class="talk-abstract">
<p>
Dependent types can model and guide the implementation of various
systems, with the type checker aiding the programmer and keeping
errors out. However, if the typed model of the system is
erroneous, the type checker can also, unintentionally, create a
false sense of security. We present an example of how this kind of
mistake can be subtly hidden, along with work on integrating
QuickCheck at the type level, the result being type-driven
development with increased confidence that our types are correct.
</p>
</div>
</td>
</tr>
<tr>
<td class="time"> 15:30 – 16:00 </td>
<td> Constantine Theocharis (St Andrews) </td>
<td>
<a class="talk-title" href="javascript:toggleAbstract('abstract5')">
Customisable Representation for Logic and Data
</a>
<div id="abstract5" class="talk-abstract">
<p>
Functional programming languages with inductive data types provide
a convenient framework for the expression of pattern-matching
logic over abstract data. However, these data types (e.g. lists,
natural numbers) are commonly represented using linked trees in
most functional languages. This is not a very performant structure
for common operations such as lookup, and can often suffer from
cache locality issues. This work explores how the machine
representation of an inductive data type can be decoupled from its
actual definition, such that it can vary independently of the data
type itself. For example, heap-backed arrays can be used for
lists, and GMP-style big-integers can be used for natural numbers.
The presented system involves a translation process from a
high-level source language with inductive definitions, to a
low-level language with memory primitives such as heap boxes and
contiguous sequences. Data type representations are user-provided
and required for each data type (with fallback to linked trees).
The translation process operates on an intermediate representation
of data types which can perform non-trivial collapsing of
constructor chains into the target representation. During the
translation, specialised user-provided functions operating on a
specific representation of a data type can also be used in place
of their generalised counterparts (for example, specialising
<code>length</code> for heap-backed arrays). A categorical model
of the process is developed, and some basic meta-theoretic
properties of the translation are explored.
</p>
</div>
</td>
</tr>
<tr class="break">
<td> 16:00 – 16:30 </td>
<td colspan=2> Coffee break </td>
</tr>
<tr>
<td class="time"> 16:30 – 17:00 </td>
<td> Simon Gay (Glasgow) </td>
<td>
<a class="talk-title" href="javascript:toggleAbstract('abstract6')">
Trains and Types
</a>
<div id="abstract6" class="talk-abstract">
<p>
The problem of drawing diagrams of model train layouts gives an
elementary example of (1) an embedded domain-specific language and
(2) dependent types.
</p>
</div>
</td>
</tr>
<tr>
<td class="time"> 17:00 – 17:30 </td>
<td> Kengo Hirata (Edinburgh) </td>
<td>
<a class="talk-title" href="javascript:toggleAbstract('abstract7')">
Quantum Uncomputation as Garbage Collection
</a>
<div id="abstract7" class="talk-abstract">
<p>
In this talk, I aim to introduce my ongoing research in my PhD
program. In quantum programming languages, the qubit type must be
handled linearly, which can sometimes be cumbersome. One technique
to make it look like affine type is 'automatic uncomputation'. In
this talk, I would like to explain that uncomputation functions as
garbage collection in quantum programming languages. Additionally,
I will discuss what ideal frameworks should look like and how a
language should be designed.
</p>
</div>
</td>
</tr>
<tr class="break">
<td> 17:30 – late </td>
<td colspan=2> Pub </td>
</tr>
</table>
</section>
<section>
<h3>Organisers</h3>
General information about SPLS is available from the
<a href="https://scottish-pl-institute.github.io/spls/">SPLS page</a>.
For further information about this event, please contact
<a href="mailto:[email protected]">Chris Brown</a>,
<a href="mailto:[email protected]">Constantine Theocharis</a>,
<a href="mailto:[email protected]">Thomas E. Hansen</a>, or
<a href="mailto:[email protected]">Ellis Kesterton</a>.
Members of the SPLS community can be contacted via the
<a href="https://spls.zulipchat.com/">SPLS Zulip</a>.
</section>
</body>
</html>