This edition of SPLS will be held both in-person
and online.
The in-person meeting will take place in the
Cottrell Building, room 2A73
at the University of Stirling.
In-person event for PhD students, organised by the SPLI.
09:30 — 10:00 Breakfast & welcome
10:00 — 11:00 University & SPLI presentation
11:30 — 12:00 Live Q&A; you can send in your questions anonymously here.
12:00 — 13:00 LUNCH
13:00 — 14:00 SESSION 1: Program Transformations
Anton Lorenzen (Edinburgh)
Balanced Search Tree Insertion:
Functional is Top-down is Bottom-up
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.
Ryan Kirkpatrick (St Andrews)
Automated Thread Placement via Dynamic Binary Instrumentation
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.
14:00 — 14:30 COFFEE
14:30 — 15:30 SESSION 2: Semantics
Jacques Carette (McMaster)
Definite Folds
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.
This is joint work with my Ph.D. student, Noel Brett.
Sam Lindley (Edinburgh)
Encoding Product Types
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.
15:30 — 16:00 COFFEE
16:00 — 17:00 SESSION 3: Behavioural Types
Katarzyna Marek (Edinburgh)
A Sound and Complete View-based Regex Parser
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.
This is joint work with Ohad Kammar and James McKinna.
Simon Fowler (Glasgow)
Special Delivery: Programming with Mailbox Types
Actor-based languages such as Erlang and Elixir are
well-suited to distributed programming due to the
concept of a mailbox: 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.
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.
(joint work with Simon Gay, Phil Trinder, and Franciszek Sowul)
Please register by 20th October on the SPLS Doodle poll if you plan to attend SPLS in person.
Please register by 20th October on the PhD event Doodle poll if you plan to attend the PhD event.
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.
