(Former employee or visitor)

**Willingness to take Ph.D. students: **Yes

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

Mathematics |

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.

## Introduction to Bidirectional Transformations

Research output: Chapter in Book/Report/Conference proceeding › Chapter

## Triangulating Context Lemmas

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## On principles of Least Change and Least Surprise for bidirectional transformations

Research output: Contribution to journal › Article

## A Theory of Least Change for Bidirectional Transformations

Project: Funded Project › Research

ID: 3563672