James McKinna

56 papers A* 1B 5C 1Journal 21Unranked 26
YearRankTypeTitle / Venue / Authors
2025 J jnl
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings.
Proc. ACM Program. Lang.
Jan van Brügge, James McKinna, Andrei Popescu, Dmitriy Traytel
2025 J jnl
Call-by-value and call-by-name: A simple proof of a classic theorem.
J. Funct. Program.
Dariusz Biernacki, James McKinna, Filip Sieczkowski
2025 J jnl
The Agda standard library: version 2.0.
J. Open Source Softw.
Matthew L. Daggitt, Guillaume Allais, James McKinna, Andreas Abel, Van Doorn, Nathan, James Wood, Ulf Norell, Donnacha Oisín Kidney, Sergei Meshveliani, Sandro Stucki, Jacques Carette, Alex Rice, Jason Z. S. Hu, Li-yao Xia, Shu-Hung You, Reed Mullanix, Wen Kokke
2024 J jnl
Forward- or reverse-mode automatic differentiation: What's the difference?
Sci. Comput. Program.
Birthe van den Berg, Tom Schrijvers, James McKinna, Alexander Vandenbroucke
2023 J jnl
Structural Subtyping as Parametric Polymorphism.
CoRR
Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley
2023 J jnl
Structural Subtyping as Parametric Polymorphism.
Proc. ACM Program. Lang.
Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley
2022 J jnl
Forward- or Reverse-Mode Automatic Differentiation: What's the Difference?
CoRR
Birthe van den Berg, Tom Schrijvers, James McKinna, Alexander Vandenbroucke
2021 J jnl
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs.
J. Funct. Program.
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
2020 J jnl
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs.
CoRR
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
2020 — ed.
Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2020, Virtual Event, USA, August 23, 2020
ICFP
James McKinna, Cyrus Omar
2019 J jnl
Abstracting extensible data types: or, rows by any other name.
Proc. ACM Program. Lang.
J. Garrett Morris, James McKinna
2018 J jnl
A type and scope safe universe of syntaxes with binding: their semantics and proofs.
Proc. ACM Program. Lang.
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
2018 B conf
Triangulating context lemmas.
CPP
Craig McLaughlin, James McKinna, Ian Stark
2017 J jnl
Coalgebraic Aspects of Bidirectional Computation.
J. Object Technol.
Faris Abou-Saleh, James McKinna, Jeremy Gibbons
2017 J jnl
On principles of Least Change and Least Surprise for bidirectional transformations.
J. Object Technol.
James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
2017 B conf
Type-and-scope safe programs and their proofs.
CPP
Guillaume Allais, James Chapman, Conor McBride, James McKinna
2016 — conf
Bidirectional Transformations with Deltas: A Dependently Typed Approach (Talk Proposal).
Bx@ETAPS
James McKinna
2016 — conf
Complements Witness Consistency.
Bx@ETAPS
James McKinna
2016 — conf
How to Regain Equilibrium without Losing your Balance? Scenarios for Bx Deployment (Discussion Paper).
Bx@ETAPS
James McKinna, Perdita Stevens
2016 — conf
Introduction to Bidirectional Transformations.
Bidirectional Transformations
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
2016 — conf
Reflections on Monadic Lenses.
A List of Successes That Can Change the World
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
2016 J jnl
Reflections on Monadic Lenses.
CoRR
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
2015 — conf
Coalgebraic Aspects of Bidirectional Computation.
Bx@STAF
Faris Abou-Saleh, James McKinna, Jeremy Gibbons
2015 B conf
Notions of Bidirectional Computation and Entangled State Monads.
MPC
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
2015 J jnl
Notions of bidirectional computation and entangled state monads.
CoRR
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
2015 — conf
Towards a Principle of Least Surprise for Bidirectional Transformations.
Bx@STAF
James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
2014 — conf
Entangled State Monads.
EDBT/ICDT Workshops
James Cheney, James McKinna, Perdita Stevens, Jeremy Gibbons, Faris Abou-Saleh
2014 — conf
Towards a Repository of Bx Examples.
EDBT/ICDT Workshops
James Cheney, James McKinna, Perdita Stevens, Jeremy Gibbons
2013 — conf
Certified Complexity (CerCo).
FOPARA
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
2013 J jnl
The
Ann. Pure Appl. Log.
Herman Geuvers, Robbert Krebbers, James McKinna
2012 J jnl
The lambda-mu-T-calculus
CoRR
Herman Geuvers, Robbert Krebbers, James McKinna
2011 J jnl
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
Log. Methods Comput. Sci.
Stéphane Lengrand, Roy Dyckhoff, James McKinna
2011 — conf
Dynamic Proof Pages.
MathWikis@ITP
Carst Tankink, James McKinna
2010 — conf
Narrating Formal Proof (Work in Progress).
UITP
Carst Tankink, Herman Geuvers, James McKinna
2010 J jnl
Proviola: A Tool for Proof Re-animation
CoRR
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
2010 — conf
Proviola: A Tool for Proof Re-animation.
AISC/MKM/Calculemus
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
2010 — conf
Pure Type Systems without Explicit Contexts
LFMTP
Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk
2010 — conf
Type Inference in Context.
MSFP@ICFP
Adam Gundry, Conor McBride, James McKinna
2009 — conf
A Logically Saturated Extension of lambdaµµ.
Calculemus/MKM
Lionel Elie Mamane, Herman Geuvers, James McKinna
2009 — conf
Domain Specific Languages (DSLs) for Network Protocols (Position Paper).
ICDCS Workshops
Saleem Bhatti, Edwin C. Brady, Kevin Hammond, James McKinna
2008 — conf
A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq.
TYPES
Eelis van der Weegen, James McKinna
2008 — conf
A Real Semantic Web for Mathematics Deserves a Real Semantics.
SemWiki
Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers
2008 — conf
Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle.
AISC/MKM/Calculemus
Peter Chapman, James McKinna, Christian Urban
2007 — conf
Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types.
Trends in Functional Programming
Edwin C. Brady, James McKinna, Kevin Hammond
2006 B conf
A Sequent Calculus for Type Theory.
CSL
Stéphane Lengrand, Roy Dyckhoff, James McKinna
2006 — conf
Eliminating Dependent Pattern Matching.
Essays Dedicated to Joseph A. Goguen
Healfdene Goguen, Conor McBride, James McKinna
2006 A* conf
Why dependent types matter.
POPL
James McKinna
2004 — conf
A Few Constructions on Constructors.
TYPES
Conor McBride, Healfdene Goguen, James McKinna
2004 C conf
Functional pearl: i am not a number-i am a free variable.
Haskell
Conor McBride, James McKinna
2004 J jnl
The view from the left.
J. Funct. Program.
Conor McBride, James McKinna
2003 — conf
Inductive Families Need Not Store Their Indices.
TYPES
Edwin C. Brady, Conor McBride, James McKinna
2002 — ed.
Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers
TYPES
Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack
1999 J jnl
Some Lambda Calculus and Type Theory Formalized.
J. Autom. Reason.
James McKinna, Robert Pollack
1993 — conf
Checking Algorithms for Pure Type Systems.
TYPES
L. S. van Benthem Jutting, James McKinna, Robert Pollack
1993 B conf
Deliverables: A Categorial Approach to Program Development in Type Theory.
MFCS
James McKinna, Rod M. Burstall
1993 — conf
Pure Type Systems Formalized.
TLCA
James McKinna, Robert Pollack