S-REPLS 16

Sponsored by VeTSS, the Research Institute on Verified Trustworthy Software Systems

The South of England Regional Programming Language Seminar (S-REPLS) is a regular and informal meeting open to everyone with a professional interest — whether it be academic or commercial — in the semantics and implementation of programming languages.

The location of S-REPLS 16 is:

• Lecture Theatre 311, Department of Computing, Imperial College London, Huxley Building, 180 Queen’s Gate, London, SW7 2AZ

Register here https://forms.office.com/e/sWvG4Z1JSR

S-REPLS Schedule

Details of Speakers and Talks

Concurrency, Regions, and Region Inference in Project Verona

Sophia Drossopolou (Imperial College London) and Matthew Parkinson (Azure Research, Microsoft)

Abstract

Project Verona is a research project run by Microsoft at Azure Research in collaboration with Imperial College London and Uppsala University. We are exploring research around language and runtime design for safe scalable memory management and compartmentalisation. The core research questions we are addressing are:

• Can a language without concurrent mutation be used for scalable memory management?
• Can linear regions be combined and split dynamically to support concurrency and data-race freedom?
• Can regions be dynamically checked during program execution, thus lightening the programmer’s cognitive load?

In this talk, we will outline the concurrency model, the region system, and a dynamic region checking system built on top of Python.

Bios

Sophia Drossopoulou is a Professor at Imperial College, and works on object oriented programming language design, type systems, concurrency, and reasoning about programs. 

Mathew Parkinson is Principal Researcher at Azure Research, Microsoft. His research covers all aspects of memory safety including runtime implementations, programming language design, and verification, including the first separation logic tool, jStar.

Garbage Collection for Rust: the Finalizer Frontier

Jake Hughes (King’s College London)

Abstract

Rust is a non-Garbage Collected (GCed) language, but the lack of GC makes expressing data-structures whose values have multiple owners awkward or inefficient. Adding GC to Rust has previously required sacrificing at least one of performance, soundness, or ergonomics. One of the major challenges for practical GC for Rust is finalization: mapping existing Rust destructors to GC finalizers seems natural but introduces subtle soundness, significant performance, and irritating ergonomic issues. In this talk, I’ll introduce Alloy, a new GC for Rust, and discuss how it provides solutions for each of these issues.

Bio

Jake is a Research Associate working in the Soft-Dev group at King’s College London. He is currently working on Alloy — a garbage collector for Rust. His interests include garbage collection and Just-in-time compilation.

RustMC: Extending the GenMC Stateless Model Checker to Rust

Oliver Pearce (Royal Holloway, University of London)

Abstract

RustMC is a stateless model checker that enables verification of concurrent Rust programs. As both Rust and C/C++ compile to LLVM IR, RustMC builds on GenMC which provides a verification framework for LLVM IR. This enables the automatic verification of Rust code and any C/C++ dependencies.

In this talk, I will present the key challenges we addressed to extend GenMC. I will also demonstrate RustMC’s effectiveness at finding concurrency bugs stemming from unsafe Rust code, FFI calls to C/C++, and the incorrect use of atomic operations.

Bio

Oliver Pearce is a student at Royal Holloway’s Centre for Doctoral Training, his research focuses on Static and dynamic program analysis, specifically the verification of concurrent Rust programs and their mixed language dependencies.

Callgraph Reachability Analysis for WhatsApp Android App Health

Akos Hajdu (Meta)

Abstract

We report on an industrial use case of static callgraph reachability analysis to improve WhatsApp Android app health. We collaborated with engineers dedicated to app health to annotate/specify source code. We leveraged the Infer static analyzer to prevent regressions during code changes and to periodically find pre-existing issues on the latest revision. Within three months, the analysis prevented almost a hundred regressions to be introduced and resulted in fixes for a handful of pre-existing issues, including examples with end-user measurable impact.

Bio

Akos Hajdu is a software engineer at Meta, working on static and dynamic program analysis for WhatsApp’s codebases. Prior to Meta, Akos completed his PhD in formal methods at the Technical University of Budapest, and spent internships at CERN and SRI International.

Compositional Symbolic Execution for the Next 700 Memory Models

Andreas Loow (Imperial College London)

Abstract

I will introduce our new formalism for memory model parametric symbolic execution tools grounded in separation logic and/or incorrectness separation logic. A symbolic execution tool is memory model parametric if it can be instantiated to multiple memory models, which is an important feature to support since different memory models are used by different programming languages (e.g., different memory data types and memory actions) and different analyses (e.g., ghost state used to support fractional ownership or other types of reasoning support). Our formalism formally captures the approach to memory model parametricity of the symbolic execution platform Gillian, which is the unique selling point of Gillian compared to similar symbolic execution tools. In more detail, in our work we define a set of requirements on memory models and show that these requirements are sufficient to guarantee the soundness of our Gillian-inspired formalism when instantiated to memory models satisfying these requirements. Moreover, we instantiate our formalism with multiple memory models and prove that these memory models satisfy the requirements we have defined. Lastly, we have mechanised our results in the Rocq theorem prover.

Bio

Andreas Lööw is currently a postdoc in Philippa Gardner’s group at Imperial College London working on the formal foundations of the Gillian symbolic execution platform.

Fulminate: Testing CN Separation Logic Specifications in C

Rini Banerjee (University of Cambridge)

Abstract

Systems code (e.g. operating systems, hypervisors) forms a crucial part of our everyday computing infrastructure, with much of it written in C/C++. These languages, while ideal for low-level programming, are rather complicated to describe formally; giving programmers the ability to manage memory manually means that complex ownership patterns are present in virtually all C/C++ programs. Separation logic has become an important tool for capturing and reasoning about these ownership patterns, forming the basis of several static analysis and proof tools (e.g. CN, a verification tool for C). However, little work has been done on testing separation logic specifications in concrete execution, since at first glance, separation-logic formulas are hard to evaluate in a reasonable amount of time. In this talk I describe our work on Fulminate, a tool for executing CN separation logic specifications on concrete inputs in C.

Bio

Rini is a third-year PhD student at the Computer Laboratory at the University of Cambridge, where she is supervised by Prof Peter Sewell and Prof Neel Krishnaswami. She works as part of the REMS (Rigorous Engineering of Mainstream Systems) group at Cambridge. She is broadly interested in programming languages research, with my current focus being testing and verification for systems software. Her work aims to improve the reliability of low-level systems which lie at the software/hardware boundary.

Reachability Types, Traces and Full Abstraction

Benedict Bunting (University of Oxford)

Abstract

Type systems that offer control over sharing are seen as a promising technique for improving program safety and performance. This has been demonstrated by the recent success of Rust, whose core is based on the shared XOR mutable principle, i.e. sharing is restricted to immutable variables. This policy turns out to be quite restrictive when it comes to expressing common programming patterns involving higher-order functions and state, like those expressible in languages such as ML or Scala.

Reachability types are a recent approach to modelling sharing in higher-order languages, aiming to provide separation guarantees through typability. The contextual equivalence problem in such a setting is exacerbated by the need to consider reachability-related constraints on the allowable interactions. In particular, they might weaken the ability of contexts to observe sequentiality.

In this talk, we investigate contextual equivalence for reachability types through the lens of operational game semantics. We provide a sound trace model for a language equipped with reachability types, and show to refine it to a fully abstract one, which captures a natural notion of equivalence based on allowing terms to share functions and locations consistently with the assigned reachability annotations. We also discuss the corresponding problem of contextual approximation, along with an inequational full abstraction result. This is a first attempt at defining a fully abstract semantics for reachability types.

Bio

Benedict is a 3rd Year DPhil student at the University of Oxford, where he was previously an undergraduate, working on programming language semantics under the supervision of Andrzej Murawski. His research employs game semantics, particularly in its operational formulation, to investigate the problem of contextual equivalence. He has published results combining operational game semantics and automata to prove decidability of contextual equivalence in some settings.

Substitution, Normalization, and Formalization

Yulong Huang (University of Cambridge)

Abstract

Capture-avoiding substitution is closed for well-typed STLC terms but not for their normal forms. However, we can still define a hereditary substitution that keeps beta-reducing the new redexes which appeared after the usual substitution. This gives rise to a normalization algorithm, first introduced by Watkins et al. and later formalized in Agda by Keller and Altenkirch.

In this talk, I will present an algebraic perspective on this story, following the setup of Fiore, to view STLC terms and normal forms as presheaves over contexts and substitution as a natural transformation operator. In particular, I will show how this perspective of STLC helps to rewrite hereditary substitution into structural recursive form and improve Keller and Altenkirch’s proof of the normalization algorithm’s correctness in Agda.

Bio

Yulong is a third-year PhD student in Computer Science at the University of Cambridge with Dr Jeremy Yallop. He works on type-preserving transformation and compilation for dependent type theory – preserving the rich and expressive type specifications down to the assembly level. He is also interested in creating efficient and practical implementations of dependently typed programming languages, such as normalization by evaluation and quantitative type theory.

Automating Quarot based LLM Quantization as Program Synthesis Problem

Andrey Rybalchenko (Microsoft Research)

Abstract

Large Language Models (LLMs) are rapidly becoming a dominant AI workload. They require a vast amount of computational resources, which sparked an ongoing optimization effort to reduces the cost of running LLMs. Quantization is a promising optimization approach in this space. It contributes to the cost reduction by replacing expensive LLM operations with cheaper, but lower precision alternatives. Quarot is a state-of-the-art method for weight, activation, and key-value cache quantization. Its inner workings stand out by relying on non-trivial transformations of the computation graph of the LLM under quantization. These transformations make it difficult to apply Quarot to an on-going stream of new LLMs entering production, by requiring a team of AI experts to perform the quantization.

In this talk, I will show how we automate application of Quarot, and, as a result, accelerate the quantization process from 30 person-hours to 30 minutes per LLM. We present our approach as a program synthesis problem, which we solve using symbolic constraint solving techniques. 

This is joint work with Hari V K, James Hensman, Henry Jackson-Flux, Pashmina Cameron, and Victor Ruehle.

Bio

Andrey Rybalchenko is a researcher in the System and Networking group at Microsoft Research working on network verification and efficient AI.

Generate Formal Specifications and Explain Them to End Users

Andy Gordon (Cogna)

Abstract

What if natural language really is the next programming language? One consequence, explored in our recent TOSEM paper, is that end users themselves can use words to generate software for their tasks and processes. This software may even be formally verified – thanks to rapid advances in AI-generation of formally verified software with tools like Dafny or Lean. Still, formal verification is no cure-all. We need methods to help end users check that AI-generated logic or verified code meets their needs, especially when the end users are not at ease with maths. My talk will describe this long-established but rapidly evolving area at the intersection of programming languages, AI, and HCI. I hope to generate discussion – AI will keep improving the generation of specs, and verification of code, but we need to find ways for end users to comprehend them.

Based in part on Diana Robinson, Christian Cabrera, Andrew D. Gordon, Neil D. Lawrence, Lars Mennen, “Requirements are All You Need: The Final Frontier for End-User Software Engineering”. ACM TOSEM 2025.

Bio

Andy Gordon is a computer scientist specializing in programming languages, AI, and human-computer interaction. Andy is Science Advisor at London startup Cogna where he leads research on delivering software from natural language. Before joining Cogna as an early employee in 2023, Andy had a 26 year career at Microsoft Research. As Partner Research Manager, Andy led a diverse team of researchers and engineers to evolve Excel as an end-user programming language. He made significant contributions to the development of natural language formulas using generative AI in Copilot for Excel, formula features like LET/LAMBDA, the Calc.ts client-side execution engine for Excel formulas, and Excel Labs. Andy was recognised as a 2020 Fellow of the Association for Computing Machinery (ACM) for his research on programming languages: their principles, logic, usability, and trustworthiness. Andy is now Honorary Professor at the University of Edinburgh, following 12 years as full Professor. His PhD research at Cambridge contributed to the design of monadic I/O in Haskell, with his ASCII art “>>=” inspiring the Haskell logo.