Dr Chris Barrett

I'm a post-doctoral researcher working with Dr. Aleks Kissinger in the Quantum Group in the Dept. of Computer Science at the University of Oxford. My previous position was with Dr Dan Ghica on the EPSRC Nominal String Diagrams project within the Theory of Computation group at the University of Birmingham. I received my Ph.D. in (Theoretical) Computer Science from the University of Bath in 2023. My supervisor was Willem Heijltjes. My original background was in pure mathematics.

My research interests are in the area of proof and type theory, the lambda-calculus and programming language semantics. I am especially interested in designing calculi and type systems for computational effects, including for quantum computation. My understanding of these subjects is influenced by deep inference and by (pure and applied) category theory.

I was sole organizer of the Bath Mathematical Foundations Seminar in the years 2020-2022, and co-organizer of the Birmingham Theory Seminar in 2023. I also worked as a teaching assistant at the University of Bath for modules in Foundations of Computation, Functional Programming, and Analytical Mathematics for Applications in the years 2018-2021.

ORCID iD | Google Scholar | LinkedIn | e-mail | CV

The Functional Machine Calculus II: Semantics

Chris Barrett, Willem Heijltjes, Guy McCusker

Computer Science Logic 2023

The Functional Machine Calculus (FMC), recently introduced by Heijltjes, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects. In this paper, we explore the denotational semantics of the FMC.

We have three main contributions: first, we argue that its syntax -- in which both effects and lambda-calculus are realised using the same syntactic constructs -- is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy's proof for the lambda-calculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.

Presented at the NIETS workshop and Computer Science Logic (CSL) 2023.

Paper (Conference) | Slides (NIETS'22, CSL'23)

A Subatomic Proof System for Decision Trees

Chris Barrett, Alessio Guglielmi

Transactions on Computational Logic 2022

We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. The system exhibits remarkable proof-theoretical naturalness: the system consists of all and only the inference rules generated by the single, simple, linear scheme of the recently introduced subatomic logic (pictured, right).

Thanks to this regularity, cuts are eliminated via a natural construction. By expanding the language of propositional logic, we make its proof theory more regular and generate more proofs, some of which are very efficient. That design is made possible by considering atoms as superpositions of their truth values, which are connected by self-dual, non-commutative connectives. To accommodate self-dual non-commutativity, we compose proofs in deep inference.

Presented at Structures and Deduction, a satellite workshop of FSCD 2019.

Paper (Journal) | Slides (S&D'19)

Ph.D. Thesis: On the Simply Typed Functional Machine Calculus: Categorical Semantics and Strong Normalisation

Thesis advisor: Willem Heijltjes

Department of Computer Science, University of Bath, December 2022

The Functional Machine Calculus (FMC) was recently introduced as a generalization of the lambda-calculus to include higher-order global state, probabilistic and non- deterministic choice, and input and ouput, while retaining confluence. The calculus can encode both the call-by-name and call-by-value semantics of these effects. This is enabled by two independent generalizations, both natural from the perspective of the FMC’s operational semantics, which is given by a simple (multi-)stack machine.

The first generalization decomposes the syntax of the lambda-calculus in a way that allows for sequential composition of terms and the encoding of reduction strate- gies. Specifically, there exist translations of the call-by-name and call-by-value lambda-calculus which preserve operational semantics. The second parameterizes application and abstraction in terms of ‘locations’ (corresponding to the multiple stacks of the machine), which gives a unification of the operational semantics, syn- tax, and reduction rules of the given effects with those of the lambda-calculus. The FMC further comes equipped with a simple type system which restricts and captures the behaviour of effects.

This thesis makes two main contributions, showing that two fundamental prop- erties of the lambda-calculus are preserved by the FMC. The first is to show that the categorical semantics of the FMC, modulo an appropriate equational theory, is given by the free Cartesian closed category. The equational theory is validated by a notion of observational equivalence. The second contribution is a proof that typed FMC-terms are strongly normalising. This is an extension (and small simplification) of Gandy’s proof for the lambda-calculus, which additionally emphasizes its latent operational intuition.

Presented at the Birmingham, Oxford and Cambridge University Theory seminars.

Thesis | Slides (Viva) | Slides (Birmingham, Oxford, Cambridge Theory Seminars '22/'23)

Masters' Project: On the Quantized Dynamics of Factorial Languages

Chris Barrett, Evgenios Kakariadis

The Quarterly Journal of Mathematics 2017

For my masters' project at Newcastle University I researched and wrote an introduction to Symbolic Dynamics, including some Haskell code to generate "follower set graphs" -- finite representations of certain spaces of infinite sequences. This code was used to falsify a conjecture and was part of my small contribution to the above published mathematics paper. The work was awarded the Best MMath Project school prize.

Paper (Journal) | Dissertation | Poster | Github