Martin Churchill

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.

Publications

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.
Modular Semantics for Transition System Specifications with Negative Premises by Martin Churchill, Peter D. Mosses and Mohammad Mousavi – presented at CONCUR 2013 [pdf] with additional material here
Modular Bisimulation Theory for Computations and Values by Martin Churchill and Peter D. Mosses – presented at FoSSaCS 2013 [pdf] with additional material here
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]

Other Articles

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]

Selected Talks

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]

Tools

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

Imperative Programs as Proofs via Game Semantics – PhD thesis at the University of Bath. My PhD advisors were Jim Laird and Guy McCusker. [opus, e-reader friendly pdf]
Abstract Semantics for a Simple Quantum Programming Language – masters thesis for MFOCS course at Oxford. My MSc thesis advisor was Samson Abramsky. [pdf]
Introduction to Fractal Geometry – a non-technical undergraduate essay, aimed at a general audience. [pdf]

Groups

PLanCompS, a 4-year joint research project based at Swansea, Royal Holloway and City
Theory Group at the University of Swansea (formerly organised the seminar series)
Wessex Theory Seminar
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
Mathematical Foundations Group at the University of Bath (formerly organised the seminar series)
Some bands: BeaconHawk and Paragon. And some audio plays.

Teaching

I have previously acted as a tutor for the following courses:

Object orientated programming, Databases (practical demonstrator, University of Oxford)
Programming 1 (lab tutor, University of Bath)
Discrete Mathematics, Analytical Mathematics for Computation, Algebra (class tutor, University of Bath)