| 2008 |
|---|
| 13 | EE | Peter Chapman,
James McKinna,
Christian Urban:
Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle.
AISC/MKM/Calculemus 2008: 38-52 |
| 12 | EE | Cezary Kaliszyk,
Pierre Corbineau,
Freek Wiedijk,
James McKinna,
Herman Geuvers:
A Real Semantic Web for Mathematics Deserves a Real Semantics.
SemWiki 2008 |
| 2006 |
|---|
| 11 | EE | Stéphane Lengrand,
Roy Dyckhoff,
James McKinna:
A Sequent Calculus for Type Theory.
CSL 2006: 441-455 |
| 10 | EE | Healfdene Goguen,
Conor McBride,
James McKinna:
Eliminating Dependent Pattern Matching.
Essays Dedicated to Joseph A. Goguen 2006: 521-540 |
| 9 | EE | James McKinna:
Why dependent types matter.
POPL 2006: 1 |
| 2004 |
|---|
| 8 | EE | Conor McBride,
Healfdene Goguen,
James McKinna:
A Few Constructions on Constructors.
TYPES 2004: 186-200 |
| 7 | EE | Conor McBride,
James McKinna:
The view from the left.
J. Funct. Program. 14(1): 69-111 (2004) |
| 2003 |
|---|
| 6 | EE | Edwin Brady,
Conor McBride,
James McKinna:
Inductive Families Need Not Store Their Indices.
TYPES 2003: 115-129 |
| 2002 |
|---|
| 5 | | Paul Callaghan,
Zhaohui Luo,
James McKinna,
Robert Pollack:
Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers
Springer 2002 |
| 1999 |
|---|
| 4 | | James McKinna,
Robert Pollack:
Some Lambda Calculus and Type Theory Formalized.
J. Autom. Reasoning 23(3-4): 373-409 (1999) |
| 1993 |
|---|
| 3 | | James McKinna,
Rod M. Burstall:
Deliverables: A Categorial Approach to Program Development in Type Theory.
MFCS 1993: 32-67 |
| 2 | | James McKinna,
Robert Pollack:
Pure Type Systems Formalized.
TLCA 1993: 289-305 |
| 1 | | L. S. van Benthem Jutting,
James McKinna,
Robert Pollack:
Checking Algorithms for Pure Type Systems.
TYPES 1993: 19-61 |
