S-REPLS 19

Overview

S-REPLS is a series of informal meetings for people in the South of England interested in the principles, design and implementation of programming languages. Events take place approximately thrice yearly, organised by members of the community.

Date and location

Registration

Provisional Schedule

1000-1100 Keynote: Vellvm: Formal Verification of LLVM IR Code
Steve Zdancewic (University of Pennsylvania)

Biography

Dr. Zdancewic is the Schlein Family President's Distinguished Professor in the Computer and Information Science Department at the University of Pennsylvania. He received his Ph.D. in Computer Science from Cornell University in 2002, and he graduated from Carnegie Mellon University with a B.S. in Computer Science and Mathematics in 1996. He is the recipient of an NSF Graduate Research Fellowship, an Intel fellowship, an NSF CAREER award, a Sloan Fellowship, and a Lindback Foundation Award for Distinguished Teaching. His numerous publications in the areas of programming languages and computer security include several best paper awards.

Abstract

LLVM is an industrial-strength compiler that's used for everything from iOS development to academic research. However, like any piece of complicated software, LLVM IR itself has a complex specification, making it hard to fully understand, and its implementation has bugs, which can cause potentially catastrophic mis-compilation errors. These properties make the LLVM framework a sweet spot for bug-finding and verification technologies--any improvements to it are amplified across its many applications.

This talk will survey the Vellvm (Verified LLVM) project, which aims to define a formal, mathematical specification for a large, useful subset of LLVM. Vellvm is implemented in the Rocq interactive theorem prover, which can be used for developing machine-checkable properties about LLVM IR programs and compiler optimization passes. Along the way, we'll explore some subtleties of LLVM IR semantics and see how Vellvm models them in a modular way by composing "monadic interpreters" built on top of a data structure called _interaction trees_. We'll also see some applications of Vellvm for verified compiler construction.

1100-1130 Break

 

1130-1200 The LLMbda Calculus: AI Agents, Conversations, and Information Flow
Andrew D. Gordon (University of Edinburgh)

Abstract

A conversation with a large language model (LLM) is a sequence of prompts and responses, with each response generated from the preceding conversation. AI agents build such conversations automatically: given an initial human prompt, a planner loop interleaves LLM calls with tool invocations and code execution. This tight coupling creates a new and poorly understood attack surface. A malicious prompt injected into a conversation can compromise later reasoning, trigger dangerous tool calls, or distort final outputs. Despite the centrality of such systems, we currently lack a principled semantic foundation for reasoning about their behaviour and safety. We address this gap by introducing an untyped call-by-value lambda calculus enriched with dynamic information-flow control and a small number of primitives for constructing prompt-response conversations. Our language includes a primitive that invokes an LLM: it serializes a value, sends it to the model as a prompt, and parses the response as a new term. This calculus faithfully represents planner loops and their vulnerabilities, including the mechanisms by which prompt injection alters subsequent computation. The semantics explicitly captures conversations, and so supports reasoning about defenses such as quarantined sub-conversations, isolation of generated code, and information-flow restrictions on what may influence an LLM call. A termination-insensitive noninterference theorem establishes integrity and confidentiality guarantees, demonstrating that a formal calculus can provide rigorous foundations for safe agentic programming.

Based on joint work with Zac Garby (Nottingham) and David Sands (Chalmers).

1200-1230 Dependent Multiplicities in Dependent Linear Type Theory
Maximilian Dore (University of Oxford)

Abstract

One of the use cases of linear types is for program specification, e.g., in a linear type system, any function between lists is necessarily a permutation, which makes it straightforward to verify that a sorting program is correct. However, few functional programs are linear in this way. Quantitative type theory (QTT) improves the picture and allows, e.g., for adequately typing projection functions by giving the dropped variables a 0-multiplicity. But still, only few programs use their inputs in a way that can be captured statically. I will present a dependent linear type theory in which multiplicities are not taken from a static resource algebra, but are instead (open) terms of the natural numbers, which allows for giving precise resource annotations to a large range of programs which involve branching and recursion. The type theory arises as an embedding of linear logic in dependent type theory and has straightforward denotational semantics. I will close with some discussion of possible further applications of embedding substructural logics in dependent type theory.

1230-1400 Lunch

 

1400-1430 Indexical Reasoning About Imperative Data: Why Fold if you can Crimp?
Jamie Kai (University of British Columbia, Canada)

Abstract

Inductive definitions are ubiquitous for program verification, but mismatches between the recursion order of inductive definitions often necessitate substantial manual proofs. This is especially unfortunate when reasoning about common properties whose meaning is not order-sensitive, such as sums, maximal elements or (multi)set contents of a data structure, and exacerbated by stateful models of data in imperative programming.

Our work presents an alternative to explicit inductive reasoning for such situations. This comprises two novel techniques: a higher-order crimp operator, and a logic of indexicals. The crimp operator is a generalization of an associative and commutative fold, whose instantiations express diverse order-insensitive properties of a variety of inductive and cyclic data structures. The logic of indexicals encodes key laws for positional reasoning about data in terms of the crimp operator. We examine indexicals from the perspective of local reasoning, and derive an efficient indexical framing method in an abstract separation logic. Our techniques are implemented in a first-order deductive verification tool; we demonstrate their efficiency and automation on selected program verification challenges from the literature.

1430-1500 Precomputation: A New Era in Multi-Stage Programming
Hossein Haeri (PLWorkz R&D, Belgium)

Abstract

Precomputate-time is a novel stage in its Multi-Stage Programming (MSP) sense that lies between compile-time and runtime. Precomputation is incorporated in the Xlang build toolchain, where Xlang is a new systems programming language being developed in the industry. Unlike traditional MSP, precomputation takes no metalevel syntax; neither does its usage take compiler construction or formal semantics expertise. Xlang achieves that via a paradigm shift in the programming model of MSP. While traditional MSP builds on Davies’ toolkit, Xlang’s model is similar to that of Glück and Jørgensen, which, in turn, is a generalization of Jones’ model for partial evaluation.

Despite its potential for boosting efficiency dramatically, MSP was never widely deemed affordable even in rather academic languages. In this talk, we show how Xlang’s paradigm shift can finally make MSP available to mainstream programming.

1500-1530 Implementing Sandwood, a probabilistic programming language for Java
Daniel Goodman

Abstract

Sandwood is a Java inspired probabilistic programming language, compiler, and supporting libraries. Bayesian models constructed in Sandwood are compiled to Java objects which can be included as discrete components within a system. The decision to compile models from a Java like language has lots of advantages, but presented the problem writing code at compile time to enforce the relationships between variables at runtime in a way that is both efficient and user friendly to the developers writing code generation code for the compiler. This talk takes a high level look at some of the techniques developed.

1530-1600 Break

 

1600-1630 Contextual Embeddings: Implementing Bound Variables through Instance Resolution
Samantha Frohlich (University of Bristol)

Abstract

Representing bound variables in embedded languages is a challenging problem, often requiring painful trade-offs between expressivity and usability. On the one hand, first-order representations using de Bruijn indices have many nice properties, but quickly become difficult to read and write. On the other hand, higher-order representations can piggy-back on the host language's binders to offer a more ergonomic interface, at a variety of costs depending on the technique. The current state-of-the-art is unembedding, i.e. a translation from the higher-order representation to the first-order and back again to get the best of both worlds. Unfortunately, the fact that this translation is type-safe relies on external metatheoretic arguments, holding unembedding back from its true potential. We solve this problem with a new embedding technique that uses instance resolution to define a context-directed isomorphism between an ergonomic higher-order interface and a first-order representation. Unlike previous techniques, this also applies to embedded languages with modal and substructural (e.g. linear) type systems, making unembedding relevant for modern languages.

1630-1700 Suspending and Resuming in WebAssembly
Ezra e. k. Cooper (University of Edinburgh)

Abstract

WebAssembly is a byte-code format that runs in web browsers and allows compiling a wide variety of languages to run within web pages. When the source languages have concurrency features, though, it is necessary for the compiler to perform an elaborate CPS or state-machine transformation. However, newly proposed extensions, called WasmFX and inspired by effect-handler constructs, allow a more direct compilation style. We've been working on validating these extensions by adding them to new compiler backends and running benchmarks to assess their performance. We'll discuss some of the challenges of porting a compiler (Go) that already uses a state-machine transformation, and talk about performance measurement of the cutting-edge implementations.

1700 Close

Mailing list

Questions

• Tobias Grosser (tobias.grosser@cst.cam.ac.uk)
• Jeremy Yallop (jeremy.yallop@cl.cam.ac.uk)