We acknowledge and are grateful for the continued sponsorship of SPLS by the Scottish Informatics and Computer Science Alliance (SICSA)
The talks will be held on the North Haugh, in the Willie Russell Building, lecture theatre C.
There is a channel, #spls-2024-03, set up on the SPLS Zulip chat service.
Time | Speaker | Title |
---|---|---|
12:00 – 12:45 | Lunch | |
12:45 – 13:15 | Andy Gordon (Cogna Ltd and University of Edinburgh) |
Rise of the AI-Empowered End User Software Engineer
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. |
13:15 – 13:45 | Ferdia McKeogh (St Andrews) |
How to Compile a Compiler
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. |
13:45 – 14:15 | Ellis Kesterton (St Andrews) |
Zero Cost Higher-Order Functions
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. |
14:15 – 14:30 | Coffee break | |
14:30 – 15:00 | Meven Lennon-Bertrand (Cambridge) |
Definitional Functoriality for Dependent (Sub)Types
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 coercions. 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. |
15:00 – 15:30 | Thomas Hansen (St Andrews) |
Increasing confidence in Types
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. |
15:30 – 16:00 | Constantine Theocharis (St Andrews) |
Customisable Representation for Logic and Data
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
|
16:00 – 16:30 | Coffee break | |
16:30 – 17:00 | Simon Gay (Glasgow) |
Trains and Types
The problem of drawing diagrams of model train layouts gives an elementary example of (1) an embedded domain-specific language and (2) dependent types. |
17:00 – 17:30 | Kengo Hirata (Edinburgh) |
Quantum Uncomputation as Garbage Collection
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. |
17:30 – late | Pub |