This page links to work I have done in semantics of programming languages, and some other bits. My work has mainly focussed on modular semantics, game semantics, and quantum semantics. These days, I am a Software Engineer at Google.
Reusable Components of Semantic Specifications by Martin Churchill, Peter D. Mosses and Paolo Torrini – presented at Modularity 2014 [pdf] with additional material here, there's also a journal version [pdf] with Neil Sculthorpe.
Imperative Programs as Proofs via Game Semantics by Martin Churchill, James Laird and Guy McCusker – journal publication in Annals of Pure and Applied Logic 164/11[arxiv], also presented at LICS 2011 [opus]
A Logic of Sequentiality by Martin Churchill and James Laird – appeared at Computer Science Logic 2010, containing the first results of my PhD thesis [opus]
A Concrete Representation of Observational Equivalence for PCF – a result presented at the Games for Logic and Programming Languages (GaLoP) workshop in 2009. Joint work with Jim Laird and Guy McCusker. [arxiv]
Categorical Semantics for a Quantum Language – a writeup of the main result in my masters thesis. [pdf]
Computer Programs as Dialogue Games – Meeting of Minds, University of Bath, June 2009 (general audience). [pdf]
A Concrete Representation of Observational Equivalence for PCF – GaLoP workshop, March 2009. [pdf]
A Logic of Sequentiality – British Logic Colloquium, August 2009. [pdf]
Game Semantics and Agda – Osaka Software Engineering Workshop, AIST, February 2010. [pdf]
Imperative Programs as Proofs via Game Semantics – University of Birmingham, July 2011. [pdf]
Modular Bisimulation Theory for Computations and Values – FoSSaCS, Rome, March 2013. [pdf]
Modular Semantics for Open Transitions with Negative Premises – Queen Mary University of London, June 2013. [pdf]
Component-Based Dynamic Semantics for Caml Light – SLS, Microsoft Research Cambridge, June 2013. [pdf]
Customizable Delivery with the App Bundle – Google I/O, May 2019. [youtube]
Observational Equivalence Checker for Idealised Algol – OCaml implementation of ideas presented in the work of McCusker and Ghica, representing game semantics of Idealised Algol as regular expressions. [ml]
Agda Formalisation of Game Semantics and WS – Implementation of some game semantics, and our Logic of Sequentiality, in Agda. Joint work with Makoto Takeyama of AIST, Japan on these trips. There's a bit about it in my PhD thesis. [source, browsable Agda html]
Prototyped Component-based Semantics for Caml Light – Dynamic Semantics of Caml Light by translation into reusable constructs, each with independent operational semantics. The rules can be interpreted by Prolog to run real world programs. [zip]
Theses and Essays
Introduction to Fractal Geometry – a non-technical undergraduate essay, aimed at a general audience. [pdf]
PLanCompS, a 4-year joint research project based at Swansea, Royal Holloway and City
Denotational Semantics for the Evaluation Behaviour of Computer Programs, a joint project between Bath and AIST, Japan
Redesigning Logical Syntax (REDO), a joint project between Bath and INRIA
I have previously acted as a tutor for the following courses:
Programming 1 (lab tutor, University of Bath)
I am a Software Engineer at Google, London.
Before that: PhD studies at the University of Bath.
Before that: working as a software engineer at Renishaw.
Before that: MSc in Mathematics and the Foundations of Computer Science at the University of Oxford.
Before that: undergraduate degree in Maths and Computer Science at Keble College, Oxford.