This edition of SPLS will be held both in-person
and online.
The in-person meeting will take place in the
Cairn Auditorium, Postgraduate Centre
at the Heriot-Watt University.
Type-preserving compilation via dependently typed syntax
The CompCert project produced a verified
compiler for a large fragment of the C programming
language. The CompCert compiler is implemented in the
type-theoretic proof assistant Coq, and is fully
verified: there is a proof that the semantics of the
source program matches the semantics of the target
program. However, full verification comes with a price:
the majority of the formalization is concerned not with
the runnable code of the compiler, but with properties
of its components and proofs of these properties. If we
are not willing to pay the price of full verification,
can we nevertheless profit from the technology of
type-theoretic proof assistants to make our compilers
safer and less likely to contain bugs?
In this talk, I am presenting a compiler for a small
fragment of the C language using dependently-typed
syntax. A typical compiler is proceeding in
phases: parsing, type checking, code generation, and
finally, object/binary file creation. Parsing and type
checking make up the front end, which may
report syntax and type errors to the user; the other
phases constitute the back end that should only
fail in exceptional cases. After type checking
succeeded, we have to deal only with well-typed source
programs, whose abstract syntax trees can be captured
with the indexed data types of dependently-typed proof
assistants and programming languages like Agda, Coq,
Idris, Lean etc. More concisely, we shall by
dependently-typed syntax refer to the technique
of capturing well-typedness invariants of syntax trees.
Representing also typed assembly language via
dependently-typed syntax, we can write a type-preserving
compiler whose type soundness is given by
construction. In the talk, the target of
compilation is a fragment of the Java Virtual Machine
(JVM) enriched by some administrative
instructions that declare the types of local
variables. With JVM being a stack machine, instructions
are indexed not only by the types of the local
variables, but also by the types of the stack entries
before and after the instruction. However for
instructions that change the control flow, such as
unconditional and conditional jumps, we need an
additional structure to ensure type safety. Jumps are
safe if the jump target has the same machine typing than
the jump source. By machine typing we mean the
pair of the types of the local variables and the types
of the stack entries. Consequently, each label (i.e.,
jump target) needs to be assigned a machine type and can
only be targeted from a program point with the same
machine type. Technically, we represent labels as
machine-typed de Bruijn indices, and control-flow
instructions are indexed by a context of label types.
We then distinguish two types of labels:
Join points, e. g., labels of statements following
an `if-else` statement. Join points can be
represented by a `let` binding in the abstract JVM
syntax.
Looping points, e. g., labels at the beginning of a
`while` statement that allow back jumps to iterate the
loop. Those are represented by `fix` (recursion).
Using dependently-typed machine syntax, we ensure that
well-typed jumps do not miss. As a result, we obtain
a type-preserving compiler by construction, with a good
chance of full correctness, since many compiler faults
already break typing invariants. Intrinsic
well-typedness also allows us to write the compiler as a
total function from well-typed source to typed assembly,
and totality can be automatically verified by the Agda
type and termination checker.
14:00 — 14:30 COFFEE
14:30 — 15:30 SESSION 2: Effects and Communication
Wenhao Tang (Edinburgh)
Tracking Linear Continuations for Effect Handlers
Linear types and effect handlers are both useful
features for programming languages. However, they are
problematic when using together, as effect handlers may
invoke the continuations of operations zero or multiple
times, while conventional linear type systems do not
track the linearity of continuations. We present
Feffpop, a System F style calculus with linear types and
effect handlers, which uses type-and-effect system to
track linearity of continuations for operations. We
prove that it does not discard or duplicate linear
values during evaluation by defining a linearity-aware
semantics. To make it more practical, we present
λeffpop, an ML-variant of Feffpop with type inference
and no extra requirement for annotations. We also
present Qeffpop, an extension of λeffpop with a novel
form of effect system called qualified effect types,
which has better accuracy in tracking linear
continuations.
Matthew Alan Le Brun (Glasgow)
MAGπ: Types for Failure-Prone Communication
Multiparty Session Types (MPST) are a type discipline
for communication-based systems that guarantee relevant
properties, such as communication safety, deadlock
freedom and protocol compliance. In recent years,
several works have emerged which model failures and
introduce failure-handling techniques. However, such
works often make heavy assumptions on the underlying
network, e.g., assuming TCP-based communication where
messages are guaranteed to be delivered; adopting
centralised reliable nodes and ad-hoc notions of
reliability; or only addressing a single kind of failure
(such as node crash failures). In this work, we develop
MAGπ—a Multiparty, Asynchronous and Generalised
π-calculus, which is the first language and type system
to accommodate in unison: (i) the widest range of
non-Byzantine faults; (ii) a novel and most general
notion of reliability; and (iii) a theory generalised
over a spectrum of network assumptions, from the lowest
level of UDP-based network programming to the TCP-based
application level.
15:30 — 16:00 COFFEE
16:00 — 17:00 SESSION 3: Verification and Representation
Omri Isac (Hebrew University of Jerusalem)
Neural Network Verification with Proof Production
There are currently multiple techniques and tools for
verifying Deep Neural Networks (DNNs). When DNN verifiers
discover an input that triggers an error, that is easy to
confirm; but when they report that no error exists, there
is no way to ensure that the verification tool itself is
not flawed. As multiple errors have already been observed
in DNN verification tools, this calls the applicability of
DNN verification into question. In this talk, I will
present a novel mechanism for enhancing Simplex-based DNN
verifiers with proof production capabilities. We will
discuss how to create such mechanism based on an efficient
adaptation of the well-known Farkas’ lemma, combined with
mechanisms for handling piecewise-linear functions and
numerical precision errors. We will conclude by discussing
how to use the mechanism in order to improve the
performance of DNN verifiers, using conflict clauses.
Guillaume Allais (St Andrews)
A Universe for Serialised Data
In typed functional languages, one can typically only
manipulate data in a type-safe manner if it first has
been deserialised into an in-memory tree represented as
a graph of nodes-as-structs and subterms-as-pointers.
We demonstrate how we can use QTT as implemented in
Idris 2 to define a small universe of serialised
datatypes, and provide generic programs allowing users
to process values stored contiguously in buffers.
Our approach allows implementors to prove the full
functional correctness, in a correct by construction
manner, of the IO functions processing the data stored
in the buffer.
17:00 — late PUB
We have a reservation at the Haymarket pub, located next to the
Haymarket station in Edinburgh. We will take a bus there after
the seminar.
Please register by 1st March on the SPLS Doodle poll if you plan to attend SPLS in person.
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.
Travel
By bus from Edinburgh: lines 25, 34, 35 and 45 to Heriot-Watt University (34 and 35 stop right outside the PG Centre, 25 and 45 at the main entrance to campus); lines X27 and X28 stop a short walk north from campus (Hermiston Walk).
By
train: Curriehill
Station on the southern Edinburgh–Glasgow line is located within walking distance (ca. 2km) from the venue;
Edinburgh
Park Station on the northern Edinburgh–Glasgow
line is some 3km from the venue: you can catch a bus from
the Calder View stop or walk via the Union Canal footpath to
avoid A71.
