James McKinna

Available identifiers

Publication	Date of Publication	Type
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs	2021-12-27	Paper
Introduction to bidirectional transformations	2019-02-15	Paper
Reflections on monadic lenses	2016-08-17	Paper
Certified complexity (CerCo)	2016-01-07	Paper
Notions of bidirectional computation and entangled state monads	2015-08-27	Paper
The $\lambda \mu^{\mathbf{T}}$-calculus	2013-04-15	Paper
A focused sequent calculus framework for proof search in pure type systems	2011-05-26	Paper
Proviola: a tool for proof re-animation	2010-08-24	Paper
A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$	2009-07-09	Paper
A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq	2009-07-02	Paper
A Sequent Calculus for Type Theory	2009-03-12	Paper
Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle	2009-01-27	Paper
Eliminating Dependent Pattern Matching	2007-09-07	Paper
Types for Proofs and Programs	2006-11-13	Paper
Types for Proofs and Programs	2005-12-23	Paper
The view from the left	2004-09-27	Paper
Some lambda calculus and type theory formalized	2000-01-30	Paper
https://portal.mardi4nfdi.de/entity/Q4281480	1993-01-01	Paper

This page was built for person: James McKinna