Martin Churchill

I am a research assistant on the PLanCompS project at the University of Swansea, Wales. I am also in the process of concluding my PhD studies at the University of Bath. My research concerns the semantics of programming languages, in particular modular frameworks for semantics and game semantics. I have previously completed work in quantum program semantics, and worked a little in the proof assistant Agda. My PhD supervisors were Jim Laird and Guy McCusker.

Articles

• Imperative Programs as Proofs via Game Semantics by Martin Churchill, James Laird and Guy McCusker – 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, which was supervised by Samson Abramsky. [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]

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. [source, browsable Agda html]

Theses and Essays

• Abstract Semantics for a Simple Quantum Programming Language – masters thesis for MFOCS course at Oxford. [pdf]

• Introduction to Fractal Geometry – a non-technical undergraduate essay, aimed at a general audience. [pdf]

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)

Groups

• PLanCompS, a 4-year joint research project based at Swansea, Royal Holloway and City.

• Theory Group at the University of Swansea

• Mathematical Foundations Group at the University of Bath (formerly co-organiser of the seminar series)

• Wessex Theory Seminar

• Denotational Semantics for the Evaluation Behaviour of Computer Programs

• Redesigning Logical Syntax (REDO)

Other Links

• Computer Science Department, University of Swansea

• Computer Science Department, University of Bath

• Personal Homepage

Short CV

• I've just started a research position on the PLanCompS project at the University of Swansea, Wales.

• I'm also concluding my PhD studies at the University of Bath.

• Before that: working as a software engineer at Renishaw plc.

• 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.

Contact

Email: martin dot churchill at keble dot oxon dot org

Postal: Martin Churchill, Department of Computer Science, University of Bath, Bath BA2 7AY, UK.