Research

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

Recent papers

2010

• Adam Gundry, Conor McBride, and James McKinna, Type inference in context , MSFP 2010. To appear in ACM SIGPLAN. PDF. Talk. WWW.
• Carst Tankink, Herman Geuvers, and James McKinna, Narrating formal proof (work in progress) , UITP 2010. To appear in ENTCS. PDF. Talk.
• Herman Geuvers, Robbert Krebbers, James McKinna, and Freek Wiedijk, Pure Type Systems without Explicit Contexts , LFMTP 2010. To appear in EPTCS. PDF. Talk.
• Carst Tankink, Herman Geuvers, James McKinna, and Freek Wiedijk, Proviola: a tool for proof re-animation , CICM 2010. Springer LNAI 6167 pp.~440--454. PDF. Talk.
• Stephane Lengrand, Roy Dyckhoff and James McKinna, A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems , to appear in Logical Methods in Computer Science. PDF.

2009

• Lionel Mamane, Herman Geuvers and James McKinna, A logically saturated extension of lambda-bar-mu-mu-tilde, in: CICM 2009, Springer LNCS 5625, pp.405--421. PDF.
• Eelis van der Weegen and James McKinna, A Machine-checked Proof of the Average-case Complexity of Quicksort in Coq, In: Proceedings of TYPES 2008, Springer LNCS 5497, pp.256--271. PDF. WWW page.
• Saleem Bhatti, Edwin Brady, Kevin Hammond and James McKinna, Domain Specific Languages (DSLs) for Network Protocols (Position Paper) , International Workshop on Next Generation Network Architecture (NGNA2009) Montreal, June 22, 2009. PDF.
• James McKinna, Eelis van der Weegen and Dan Synek, Proof Pearl: Program-ming reachability algorithms in Coq, Long version with Appendix, Coq sources.

2008

• Peter Chapman, James McKinna and Christian Urban, Mechanising a proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle , in: Proceedings of AISC, Springer LNCS 5144. PDF.
• Pierre Corbineau, Herman Geuvers, Cezary Kaliszyk, James McKinna and Freek Wiedijk, Position paper: A real Semantic Web for mathematics deserves a real semantics , in: Proceedings of SemWiki 2008, 5th European Semantic Web Conference. CEUR Workshop Proceedings 360. PDF.
• Edwin Brady, Kevin Hammond and James McKinna, Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types , Trends in Functional Programming 8, Intellect. PDF.

2006

• Stephane Lengrand, Roy Dyckhoff and James McKinna, A Sequent Calculus for Type Theory , in: Proceedings of CSL'06, Springer LNCS 4207, pp.441--455. PDF.
• Healfdene Goguen, Conor McBride and James McKinna, Eliminating Dependent Pattern Matching , in: Algebra, Meaning and Computation: A Festschrift for Joseph Goguen, Springer LNCS 4060. PDF.
• Conor McBride, Healfdene Goguen and James McKinna, A Few Constructions on Constructors , in: Proceedings of TYPES'04, Springer LNCS 3839, pp.252--267. PDF.
• James McKinna, Invited Talk: Why Dependent Types Matter , in: POPL 2006, ACM. PDF.

2004

• Conor McBride and James McKinna, Functional Pearl: I am not a number; I am a free variable , in: Proceedings of the Haskell Workshop 2004, ACM. PDF.
• Edwin Brady, Conor McBride, and James McKinna, Inductive families need not store their indices , in: Proceedings of TYPES'03, Springer LNCS 3085, pp.115--129. PDF.
• Conor McBride and James McKinna, The view from the left , J. Functional Programming, Vol. 14(1), pp.69--111. PDF: Final version; Original version.
• Rob MacInnis, James McKinna, Josh Parsons, and Roy Dyckhoff, A mechanised environment for Frege's Begriffsschrift notation , in: MathUI, MKM 2004. PDF.

(these paragraphs permanently 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.

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

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

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

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.