In addition to my own research, I also convene the Brouwer Institute seminar. Offers of talks are always welcome!

Recent papers






Research Interests

(these paragraphs permanently under construction)


(link to publications)

EPIGRAM is a dependently-typed functional programming language which I designed with Conor McBride during 2001--2003, finally appearing in the Journal of Functional Programming (Vol. 14(1):69--111) in January 2004. Its gestation goes back much further, originally to Conor's 1995--6 MSc thesis on the inversion of inductive definitions in type theory, which I supervised under the aegis of Rod Burstall.

EPIGRAM is purposely frugal in its syntax, in part as an antidote to (and high-level representation of) the extremely verbose syntax within which we previously tried to program in raw Martin-Lof type theory with inductive families. Those are its datatypes: a very rich language, embracing GADTs, inductively defined relations and much else. Its programs are just let-bound function definitions, consisting of a (dependently-typed) signature, and a body composed of just three basic constructs:

This syntax is formally explained by elaboration into the underlying type theory, whose ambient meta-theory then provides very strong guarantees about the behaviour of sucessfully type-checked programs; in particular they must be total functions.

EPIGRAM, among many other things, is also unusual in having a sophisticated interactive type-checker to support programming (largely thanks to Conor), based on our earlier experience with the Coq, LEGO and ALF systems, and in being implementable on stock FP abstract machine architecture (thanks to my former PhD student, Edwin Brady).

Most EPIGRAM-related material is available from the website, hosted and maintained by Conor and the rest of Thorsten Altenkirch's team at the University of Nottingham.

(return to top)


(return to top)

Binding in machine-supported meta-theory

Over many years (1992--99, and sporadically thereafter) I collaborated with Randy Pollack on the formalisation of the meta-theory of Barendregt's Pure Type Systems, including a machine-checked proof in LEGO of the strengthening theorem and much, much else besides.

Of particular difficulty, and interest, to us, was the formalisation of name-carrying syntax for lambda- and Pi-bindings, inspired by Thierry Coquand (and pre-figured in the work of Gentzen and Kleene). This led us to a number of techniques which have since come to be known as "McKinna-Pollack syntax" whose basic idea (formulated in the summer of 1992) may be summarised as follows:

Similar ideas have been articulated by Pitts, Urban and others in the context of nominal logic. I have recently returned to the topic, with a paper with Conor at the 2004 Haskell Workshop.


(return to top)

Certified programs

My PhD (1988--92) under Rod Burstall, considered a very early form of what is now known as proof-carrying code or certified program, called deliverables.

They have received some attention over the years, and in particular their categorical structure has been explored, rediscovered and redeployed in a number of contexts.

At the time, I recall being very pleased with examples such as the machine-checked proof of the Chinese Remainder Theorem, in Chapter 4, but dissatisfied with the general picture. Notable developments in the same area during that period included Catherine Parent's Program tactic in the Coq system, although this has since been superseded by various other tools.

(text and links under construction)

(return to top)

(return to top)
Last modified: Tue Sep 21 11:32:44 CEST 2010