Mathematically Structured Programming Group
We also have a group photo from our away day to the Isle of Bute 2023.
Next MSP101 seminar
Indexical Reasoning About Imperative Data: Why Fold if you can Crimp?
Jamie Kai (University of British Columbia)
Thursday 16 July 2026, 15:00, LT711
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.In this talk, I propose 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 local reasoning about data in terms of the crimp operator, and supports an abstract separation logic relative to heaps, which we have implemented in Viper, an SMT-based first-order deductive verifier.
I will focus this talk on speculative connections to container types, quotient constructions and symmetries. The imperative programming paradigm treats the shape of data liberally, which raises questions about expressing invariants of heap-dependent inductive types.
See the MSP101 seminar page for a full list of future and past talks.
Research Themes
Our vision is to use mathematics to understand the nature of computation, and to turn that understanding into the next generation of programming languages.
We see the mathematical foundations of computation and programming as inextricably linked. We study one so as to develop the other. This reflects the symbiotic relationship between mathematics, programming, and the design of programming languages — any attempt to sever this connection will diminish each component.
To achieve these research goals we use ideas from the following disciplines:
- Functional Programming and Type Theory
- What does the future of programming languages look like? How does one take the logical structure of computation and turn it into a programming abstraction? Type theory allows us to do this by providing a language at an intermediate level of abstraction between a programming language and its logical foundations. Indeed, type theory could be said to be the ideas factory for programming languages.
- Logic
- Different logics are suitable for expressing and verifying different properties of programming languages or systems. We make use of a range of methods such as proof theory and coalgebra to understand the computational nature of proofs and systems intended to run without interruption. Those methods are driven by emerging problems in areas such as AI and security. We have particular strengths in modal logic, quantitative properties of systems, and logics for reasoning about concurrency.
- Category Theory
- How does one understand structure abstractly? How can one build theories that systematically build complex systems by composing descriptions of simpler ones? One uses category theory — that's how! Ideas such as monads and initial algebra semantics attest to the deep contribution that category theory has made to computation.