Edinburgh Research Explorer

Dr James McKinna

(Former employee or visitor)

Profile photo

Willingness to take Ph.D. students: Yes

Research Interests

James McKinna is interested in: bidirectional transformations; functional programming; dependent types; lambda calculus; interactive theorem proving; formalised mathematics


1988-1992 PhD University of Edinburgh
  Thesis title: Deliverables: a categorical approach to program development in type theory
1987-1988 MSc University of Bristol
  Mathematical Logic and Theory of Computation
1981-1985 BA Hons University of Cambridge


James McKinna received a BA in Mathematics from Cambridge (1985) (and subsequent MA (1986)), an MSc in Mathematical Logic and Theory of Computation from Bristol (1988) and a PhD in Theory of Computation from Edinburgh (1992). His PhD focused on program development in Martin-Lof type theory, based on categorical ideas of Rod Burstall, in whose group he worked until 1998, when he toook up a Lectureship at Durham. He has since held a variety of posts in Britain, and was until 2011 Assistant Professor in Computer Mathematics at Radboud Universiteit Nijmegen in the Netherlands.

Dr. McKinna has been principal or co-investigator on a number of grants in the field of type theory, interactive theorem proving and dependently-typed functional programming; with Conor McBride, he developed the influential EPIGRAM programming language. Most recently, as a Senior Research Fellow, he is a co-investigator with Perdita Stevens and James Cheney on an EPSRC project studying bidirectional transformations.

Research outputs

  1. Coalgebraic Aspects of Bidirectional Computation

    Research output: Contribution to journalArticle

  2. Type-and-Scope Safe Programs and Their Proofs

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

View all (31) »

ID: 3563672