dr. James McKinna

Contact details:
Grondslagen / Intelligent Systems
ICIS / FNWI,
Radboud Universiteit Nijmegen
Heijendaalseweg 135
6525 AJ Nijmegen
The Netherlands

e: james DOT mckinna AT cs DOT ru DOT nl
t: +31 24 365 26 10 (x52610 internally)

I am now Assistant Professor in Computer Mathematics in the Foundations Group of ICIS at the Radboud University, Nijmegen. Until recently, I held the position of Senior Teaching Fellow in Computer Science at St.Andrews in Scotland, having moved there in 2003 from a Lectureship at Durham University. Prior to that, I was a PhD student and then a post-doc in Rod Burstall's group at the LFCS in Edinburgh (1988--98).

Research

Recent talks

2009

• Scottish Theorem Provers Seminar, St. Andrews, 2009-06-12. Program-ming with Computational Induction, Slides
• Mathematical Logic in the Netherlands, Nijmegen, 2009-05-26. Proof Search in Dependently-Typed Programming, Slides.

Recent publications/submissions

2009

• Eelis van der Weegen and James McKinna, A Machine-checked Proof of the Average-case Complexity of Quicksort in Coq, Proceedings of TYPES 2008, LNCS 5497, to appear. PDF: Final version. WWW page.
• James McKinna, Eelis van der Weegen and Dan Synek, Proof Pearl: Program-ming reachability algorithms in Coq, Long version with Appendix, Coq sources.
• Herman Geuvers, James McKinna and Freek Wiedijk, Pure Type Systems without Explicit Contexts, submitted to TLCA 2009. PDF: Submitted version.
• Lionel Mamane, Herman Geuvers and James McKinna, A logically saturated extension of lambda-bar-mu-mu-tilde, accepted for MKM 2009. PDF: Submitted version.

What I do

My research interests and experience embrace Functional Programming, Computational Logic, and Formalised Mathematics, with a particular emphasis on varieties of dependent type theory as a basis for the design and implementation of integrated languages for verified programming and mathematical proof.

Some of my most recent research has involved the design, implementation and application of the dependently-typed functional programming language EPIGRAM, in collaboration with Conor McBride and others, including my former PhD student Edwin Brady.

I was an invited speaker (abstract here) at the 33rd ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages, POPL'06, Charleston, South Carolina, January 11th--13th, 2006.

Teaching

In Semester 1, 2007--08, I am

• assisting prof. dr. Barendregt with the Huygenscollege "Reflectie";

(these paragraphs under construction)

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:

• definitional steps, expressing the current function instance f t1 ... tn in terms of existing definitions, and structurally recursive calls on f;
• data decomposition steps, which generalise constructor-based case analysis; here the power of the type system lies in being able, on the one hand, to constrain or specialise types based on a given case ("learning by testing"); and on the other, to instantiate arguments to such case constructs based on the proposed type;
• local definition steps, which generalise Peyton Jones' pattern guards in Haskell; the tricky part is to ensure that such intermediate computations be abstracted from the types of their enclosing scopes, so that subsequent case analysis on the intermediate computation can further refine such types.

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.

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:

• that, informally at least, the end-judgments of derivation trees in any formal system with name-carrying binding should be invariant under automorphisms of the set of names (and hence of the derivations) which leave (the names occurring free in) the end-judgment intact;
• that this invariance principle may be reified in the proof of (judgmental) equivalence of two inductive presentations of the formal system: one weak, in which bound names are existentially bound in the premises of binding rules; and one strong, in which they are universally bound (at the meta-level); this proof amounts to a proof of closure under renaming;
• that induction (elimination) for the strong presentation, coupled with introduction of the weak, captures informally what we mean by "reasoning modulo choice of bound names".

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)

(links under construction)

• James McKinna and Edwin Brady. Phase Distinctions in the Compilation of EPIGRAM, submitted to FLOPS'06. A longer version of this paper was submitted elsewhere earlier that year.
• Healfdene Goguen, Conor McBride and James McKinna. Eliminating Dependent Pattern Matching, in: K. Futatsugi et al. (eds) Goguen Festschrift, LNCS 4060, Springer Verlag, 2006.
• Conor McBride, Healfdene Goguen and James McKinna. Some Constructions on Constructors, in Proceedings of TYPES'04, Springer LNCS 3839, 2005.
• Edwin Brady, Conor McBride and James McKinna. Inductive Families need not store their Indices, in Proceedings of TYPES'03, Springer LNCS 3085, 2004.
• Conor McBride and James McKinna. The View From the Left, J. Functional Programming, Vol.14(1), pages 69--111, Jan 2004. This paper began life in 2000--01 in a very different form; we still think it worth reading as one of the only introductions to our perspective on interactive program development.
• James McKinna. McCarthy-Painter Induction, Slides of a talk given at a 2003 Scottish Theorem Provers meeting, St. Andrews.
• James McKinna and Conor McBride. Views for Recursion, Slides of a talk given at the 2002 TYPES workshop on Termination, Hindas, Sweden.
• Conor McBride and James McKinna. Seeing and Doing, Slides of a talk given at the 2002 TYPES workshop on Termination, Hindas, Sweden.

• Conor McBride and James McKinna. I Am Not a Number; I Am a Free Variable, in Proceedings of the 2004 ACM SIGPLAN Haskell Workshop, 2004.
• James McKinna and Randy Pollack. Some Lambda Calculus and Type Theory Formalized, in J. Automated Reasoning, Vol.~23, pp.373--409, Kluwer 1999.
• Healfdene Goguen and James McKinna. Candidates for Substitution, LFCS Technical Report ECS-LFCS-97-358, Edinburgh 1997.
• Bert van Benthem Jutting, James McKinna and Randy Pollack. Checking Algorithms for Pure Type Systems, in Proceedings of TYPES'93, Springer LNCS 806, 1994.
• James McKinna and Randy Pollack. Pure Type Systems Formalized, in Proceedings of TLCA'93, Springer LNCS 664, 1993.