James McKinna

Publication Activity (10 Years)

Years Active: 1993-2024
Publications (10 Years): 18

Top Topics

Top Venues

Proc. ACM Program. Lang.

Publications

Birthe van den Berg, Tom Schrijvers, James McKinna, Alexander Vandenbroucke
Forward- or reverse-mode automatic differentiation: What's the difference? Sci. Comput. Program. 231 (2024)
Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley
Structural Subtyping as Parametric Polymorphism. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley
Structural Subtyping as Parametric Polymorphism. CoRR (2023)
Birthe van den Berg, Tom Schrijvers, James McKinna, Alexander Vandenbroucke
Forward- or Reverse-Mode Automatic Differentiation: What's the Difference? CoRR (2022)
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program. 31 (2021)
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs. CoRR (2020)
J. Garrett Morris, James McKinna
Abstracting extensible data types: or, rows by any other name. Proc. ACM Program. Lang. 3 (POPL) (2019)
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
A type and scope safe universe of syntaxes with binding: their semantics and proofs. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Craig McLaughlin, James McKinna, Ian Stark
Triangulating context lemmas. CPP (2018)
Guillaume Allais, James Chapman, Conor McBride, James McKinna
Type-and-scope safe programs and their proofs. CPP (2017)
James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
On principles of Least Change and Least Surprise for bidirectional transformations. J. Object Technol. 16 (1) (2017)
Faris Abou-Saleh, James McKinna, Jeremy Gibbons
Coalgebraic Aspects of Bidirectional Computation. J. Object Technol. 16 (1) (2017)
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
Reflections on Monadic Lenses. CoRR (2016)
James McKinna, Perdita Stevens
How to Regain Equilibrium without Losing your Balance? Scenarios for Bx Deployment (Discussion Paper). Bx@ETAPS (2016)
James McKinna
Bidirectional Transformations with Deltas: A Dependently Typed Approach (Talk Proposal). Bx@ETAPS (2016)
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
Introduction to Bidirectional Transformations. Bidirectional Transformations (2016)
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
Reflections on Monadic Lenses. A List of Successes That Can Change the World (2016)
James McKinna
Complements Witness Consistency. Bx@ETAPS (2016)
James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
Towards a Principle of Least Surprise for Bidirectional Transformations. Bx@STAF (2015)
Faris Abou-Saleh, James McKinna, Jeremy Gibbons
Coalgebraic Aspects of Bidirectional Computation. Bx@STAF (2015)
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
Notions of Bidirectional Computation and Entangled State Monads. MPC (2015)
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
Notions of bidirectional computation and entangled state monads. CoRR (2015)
James Cheney, James McKinna, Perdita Stevens, Jeremy Gibbons
Towards a Repository of Bx Examples. EDBT/ICDT Workshops (2014)
James Cheney, James McKinna, Perdita Stevens, Jeremy Gibbons, Faris Abou-Saleh
Entangled State Monads. EDBT/ICDT Workshops (2014)
Herman Geuvers, Robbert Krebbers, James McKinna
-calculus. Ann. Pure Appl. Log. 164 (6) (2013)
Roberto M. Amadio, Nicholas Ayache, François Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark, Paolo Tranquilli
Certified Complexity (CerCo). FOPARA (2013)
Herman Geuvers, Robbert Krebbers, James McKinna
The lambda-mu-T-calculus CoRR (2012)
Carst Tankink, Herman Geuvers, James McKinna
Narrating Formal Proof (Work in Progress). Electron. Notes Theor. Comput. Sci. 285 (2012)
Stéphane Lengrand, Roy Dyckhoff, James McKinna
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems Log. Methods Comput. Sci. 7 (1) (2011)
Carst Tankink, James McKinna
Dynamic Proof Pages. MathWikis@ITP (2011)
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus (2010)
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
Proviola: A Tool for Proof Re-animation CoRR (2010)
Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk
Pure Type Systems without Explicit Contexts LFMTP (2010)
Adam Gundry, Conor McBride, James McKinna
Type Inference in Context. MSFP@ICFP (2010)
Saleem Bhatti, Edwin C. Brady, Kevin Hammond, James McKinna
Domain Specific Languages (DSLs) for Network Protocols (Position Paper). ICDCS Workshops (2009)
Lionel Elie Mamane, Herman Geuvers, James McKinna
A Logically Saturated Extension of lambdaµµ. Calculemus/MKM (2009)
Peter Chapman, James McKinna, Christian Urban
Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. AISC/MKM/Calculemus (2008)
Eelis van der Weegen, James McKinna
A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. TYPES (2008)
Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers
A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki (2008)
Edwin C. Brady, James McKinna, Kevin Hammond
Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types. Trends in Functional Programming (2007)
Stéphane Lengrand, Roy Dyckhoff, James McKinna
A Sequent Calculus for Type Theory. CSL (2006)
Healfdene Goguen, Conor McBride, James McKinna
Eliminating Dependent Pattern Matching. Essays Dedicated to Joseph A. Goguen (2006)
James McKinna
Why dependent types matter. POPL (2006)
Conor McBride, James McKinna
Functional pearl: i am not a number-i am a free variable. Haskell (2004)
Conor McBride, James McKinna
The view from the left. J. Funct. Program. 14 (1) (2004)
Conor McBride, Healfdene Goguen, James McKinna
A Few Constructions on Constructors. TYPES (2004)
Edwin C. Brady, Conor McBride, James McKinna
Inductive Families Need Not Store Their Indices. TYPES (2003)
James McKinna, Robert Pollack
Some Lambda Calculus and Type Theory Formalized. J. Autom. Reason. 23 (3-4) (1999)
James McKinna, Robert Pollack
Pure Type Systems Formalized. TLCA (1993)
James McKinna, Rod M. Burstall
Deliverables: A Categorial Approach to Program Development in Type Theory. MFCS (1993)
L. S. van Benthem Jutting, James McKinna, Robert Pollack
Checking Algorithms for Pure Type Systems. TYPES (1993)