SPLS — 6th March 2024 (12:00–17:30)

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.

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.

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.

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.

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.

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 length for heap-backed arrays). A categorical model of the process is developed, and some basic meta-theoretic properties of the translation are explored.

The problem of drawing diagrams of model train layouts gives an elementary example of (1) an embedded domain-specific language and (2) dependent types.

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.