Deliverables: A Categorial Approach to Program Development in Type Theory. - James McKinna; Rod M. Burstall (MFCS, 1993)

Pure Type Systems Formalized. - James McKinna; Robert Pollack (TLCA, 1993)

Checking Algorithms for Pure Type Systems. - L. S. van Benthem Jutting; James McKinna; Robert Pollack (TYPES, 1993)

Some Lambda Calculus and Type Theory Formalized. - James McKinna; Robert Pollack (J. Autom. Reason., 1999)

Inductive Families Need Not Store Their Indices. - Edwin C. Brady; Conor McBride; James McKinna (TYPES, 2003)

Functional pearl: i am not a number-i am a free variable. - Conor McBride; James McKinna (Haskell, 2004)

A Few Constructions on Constructors. - Conor McBride; Healfdene Goguen; James McKinna (TYPES, 2004)

The view from the left. - Conor McBride; James McKinna (J. Funct. Program., 2004)

Eliminating Dependent Pattern Matching. - Healfdene Goguen; Conor McBride; James McKinna (Essays Dedicated to Joseph A. Goguen, 2006)

A Sequent Calculus for Type Theory. - Stéphane Lengrand; Roy Dyckhoff; James McKinna (CSL, 2006)

Why dependent types matter. - James McKinna (POPL, 2006)

Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types. - Edwin C. Brady; James McKinna; Kevin Hammond (Trends in Functional Programming, 2007)

Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. - Peter Chapman; James McKinna; Christian Urban (AISC/MKM/Calculemus, 2008)

A Real Semantic Web for Mathematics Deserves a Real Semantics. - Cezary Kaliszyk; Pierre Corbineau; Freek Wiedijk; James McKinna; Herman Geuvers (SemWiki, 2008)

A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. - Eelis van der Weegen; James McKinna (TYPES, 2008)

Domain Specific Languages (DSLs) for Network Protocols (Position Paper). - Saleem Bhatti; Edwin C. Brady; Kevin Hammond; James McKinna (ICDCS Workshops, 2009)

A Logically Saturated Extension of lambdaµµ. - Lionel Elie Mamane; Herman Geuvers; James McKinna (Calculemus/MKM, 2009)

Proviola: A Tool for Proof Re-animation. - Carst Tankink; Herman Geuvers; James McKinna; Freek Wiedijk (AISC/MKM/Calculemus, 2010)

Type Inference in Context. - Adam Gundry; Conor McBride; James McKinna (MSFP@ICFP, 2010)

Pure Type Systems without Explicit Contexts - Herman Geuvers; Robbert Krebbers; James McKinna; Freek Wiedijk (LFMTP, 2010)

Narrating Formal Proof (Work in Progress). - Carst Tankink; Herman Geuvers; James McKinna (UITP, 2010)

Dynamic Proof Pages. - Carst Tankink; James McKinna (MathWikis@ITP, 2011)

A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems - Stéphane Lengrand; Roy Dyckhoff; James McKinna (Log. Methods Comput. Sci., 2011)

The lambda-mu-T-calculus - Herman Geuvers; Robbert Krebbers; James McKinna (CoRR, 2012)

Certified Complexity (CerCo). - Roberto M. Amadio; Nicholas Ayache; François Bobot; Jaap Boender; Brian Campbell 001; Ilias Garnier; Antoine Madet; James McKinna; Dominic P. Mulligan; Mauro Piccolo; Randy Pollack; Yann Régis-Gianas; et al. (FOPARA, 2013)

The λμT-calculus. - Herman Geuvers; Robbert Krebbers; James McKinna (Ann. Pure Appl. Log., 2013)

Towards a Repository of Bx Examples. - James Cheney; James McKinna; Perdita Stevens; Jeremy Gibbons (EDBT/ICDT Workshops, 2014)

Entangled State Monads. - James Cheney; James McKinna; Perdita Stevens; Jeremy Gibbons; Faris Abou-Saleh (EDBT/ICDT Workshops, 2014)

Notions of Bidirectional Computation and Entangled State Monads. - Faris Abou-Saleh; James Cheney; Jeremy Gibbons; James McKinna; Perdita Stevens (MPC, 2015)

Towards a Principle of Least Surprise for Bidirectional Transformations. - James Cheney; Jeremy Gibbons; James McKinna; Perdita Stevens (Bx@STAF, 2015)

Introduction to Bidirectional Transformations. - Faris Abou-Saleh; James Cheney; Jeremy Gibbons; James McKinna; Perdita Stevens (Bidirectional Transformations, 2016)

Reflections on Monadic Lenses. - Faris Abou-Saleh; James Cheney; Jeremy Gibbons; James McKinna; Perdita Stevens (A List of Successes That Can Change the World, 2016)

Bidirectional Transformations with Deltas: A Dependently Typed Approach (Talk Proposal). - James McKinna (Bx@ETAPS, 2016)

Complements Witness Consistency. - James McKinna (Bx@ETAPS, 2016)

How to Regain Equilibrium without Losing your Balance? Scenarios for Bx Deployment (Discussion Paper). - James McKinna; Perdita Stevens (Bx@ETAPS, 2016)

Type-and-scope safe programs and their proofs. - Guillaume Allais; James Chapman 001; Conor McBride; James McKinna (CPP, 2017)

Coalgebraic Aspects of Bidirectional Computation. - Faris Abou-Saleh; James McKinna; Jeremy Gibbons (J. Object Technol., 2017)

On principles of Least Change and Least Surprise for bidirectional transformations. - James Cheney; Jeremy Gibbons; James McKinna; Perdita Stevens (J. Object Technol., 2017)

Triangulating context lemmas. - Craig McLaughlin; James McKinna; Ian Stark (CPP, 2018)

A type and scope safe universe of syntaxes with binding: their semantics and proofs. - Guillaume Allais; Robert Atkey; James Chapman 001; Conor McBride; James McKinna (Proc. ACM Program. Lang., 2018)

Abstracting extensible data types: or, rows by any other name. - J. Garrett Morris; James McKinna (Proc. ACM Program. Lang., 2019)

Structural Subtyping as Parametric Polymorphism. - Wenhao Tang; Daniel Hillerström; James McKinna; Michel Steuwer; Ornela Dardha; Rongxiao Fu; Sam Lindley (Proc. ACM Program. Lang., 2023)

Forward- or reverse-mode automatic differentiation: What's the difference? - Birthe van den Berg; Tom Schrijvers; James McKinna; Alexander Vandenbroucke (Sci. Comput. Program., 2024)

Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings. - Jan van Brügge; James McKinna; Andrei Popescu 001; Dmitriy Traytel (Proc. ACM Program. Lang., 2025)