James McKinna

According to our database, James McKinna authored at least 43 papers between 1993 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Forward- or reverse-mode automatic differentiation: What's the difference?

Birthe van den Berg, Tom Schrijvers, James McKinna, Alexander Vandenbroucke

Sci. Comput. Program., January, 2024

2023

Structural Subtyping as Parametric Polymorphism.

Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley

Proc. ACM Program. Lang., October, 2023

2019

Abstracting extensible data types: or, rows by any other name.

J. Garrett Morris, James McKinna

Proc. ACM Program. Lang., 2019

2018

A type and scope safe universe of syntaxes with binding: their semantics and proofs.

Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna

Proc. ACM Program. Lang., 2018

Triangulating context lemmas.

Craig McLaughlin, James McKinna, Ian Stark

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

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

James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens

J. Object Technol., 2017

Coalgebraic Aspects of Bidirectional Computation.

Faris Abou-Saleh, James McKinna, Jeremy Gibbons

J. Object Technol., 2017

Type-and-scope safe programs and their proofs.

Guillaume Allais, James Chapman, Conor McBride, James McKinna

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

How to Regain Equilibrium without Losing your Balance? Scenarios for Bx Deployment (Discussion Paper).

James McKinna, Perdita Stevens

Proceedings of the 5th International Workshop on Bidirectional Transformations, 2016

Complements Witness Consistency.

James McKinna

Proceedings of the 5th International Workshop on Bidirectional Transformations, 2016

Bidirectional Transformations with Deltas: A Dependently Typed Approach (Talk Proposal).

James McKinna

Proceedings of the 5th International Workshop on Bidirectional Transformations, 2016

Reflections on Monadic Lenses.

Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens

Proceedings of the A List of Successes That Can Change the World, 2016

Introduction to Bidirectional Transformations.

Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens

Proceedings of the Bidirectional Transformations, 2016

2015

Towards a Principle of Least Surprise for Bidirectional Transformations.

James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens

Proceedings of the 4th International Workshop on Bidirectional Transformations co-located with Software Technologies: Applications and Foundations, 2015

Notions of Bidirectional Computation and Entangled State Monads.

Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens

Proceedings of the Mathematics of Program Construction - 12th International Conference, 2015

2014

Entangled State Monads.

James Cheney, James McKinna, Perdita Stevens, Jeremy Gibbons, Faris Abou-Saleh

Proceedings of the Workshops of the EDBT/ICDT 2014 Joint Conference (EDBT/ICDT 2014), 2014

Towards a Repository of Bx Examples.

James Cheney, James McKinna, Perdita Stevens, Jeremy Gibbons

Proceedings of the Workshops of the EDBT/ICDT 2014 Joint Conference (EDBT/ICDT 2014), 2014

2013

The <i>λ</i><i>μ</i>^<i>T</i>-calculus.

Herman Geuvers, Robbert Krebbers, James McKinna

Ann. Pure Appl. Log., 2013

Certified Complexity (CerCo).

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

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2013

2012

The lambda-mu-T-calculus

Herman Geuvers, Robbert Krebbers, James McKinna

CoRR, 2012

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

Dynamic Proof Pages.

Carst Tankink, James McKinna

Proceedings of the ITP 2011 Workshop on Mathematical Wikis, 2011

2010

Narrating Formal Proof (Work in Progress).

Carst Tankink, Herman Geuvers, James McKinna

Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, 2010

Pure Type Systems without Explicit Contexts

Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk

Proceedings of the Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2010

Type Inference in Context.

Adam Gundry, Conor McBride, James McKinna

Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010

Proviola: A Tool for Proof Re-animation.

Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009

A Logically Saturated Extension of lambdaµµ.

Lionel Elie Mamane, Herman Geuvers, James McKinna

Proceedings of the Intelligent Computer Mathematics, 2009

Domain Specific Languages (DSLs) for Network Protocols (Position Paper).

Saleem Bhatti, Edwin C. Brady, Kevin Hammond, James McKinna

Proceedings of the 29th IEEE International Conference on Distributed Computing Systems Workshops (ICDCS 2009 Workshops), 2009

2008

A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq.

Eelis van der Weegen, James McKinna

Proceedings of the Types for Proofs and Programs, International Conference, 2008

A Real Semantic Web for Mathematics Deserves a Real Semantics.

Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers

Proceedings of the 3rd Semantic Wiki Workshop (SemWiki 2008) at the 5th European Semantic Web Conference (ESWC 2008), 2008

Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle.

Peter Chapman, James McKinna, Christian Urban

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007

Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types.

Edwin C. Brady, James McKinna, Kevin Hammond

Proceedings of the Eighth Symposium on Trends in Functional Programming, 2007

2006

Why dependent types matter.

James McKinna

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

A Sequent Calculus for Type Theory.

Stéphane Lengrand, Roy Dyckhoff, James McKinna

Proceedings of the Computer Science Logic, 20th International Workshop, 2006

Eliminating Dependent Pattern Matching.

Healfdene Goguen, Conor McBride, James McKinna

Proceedings of the Algebra, Meaning, and Computation, 2006

2004

The view from the left.

Conor McBride, James McKinna

J. Funct. Program., 2004

A Few Constructions on Constructors.

Conor McBride, Healfdene Goguen, James McKinna

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

Functional pearl: i am not a number-i am a free variable.

Conor McBride, James McKinna

Proceedings of the ACM SIGPLAN Workshop on Haskell, 2004

2003

Inductive Families Need Not Store Their Indices.

Edwin C. Brady, Conor McBride, James McKinna

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

1999

Some Lambda Calculus and Type Theory Formalized.

James McKinna, Robert Pollack

J. Autom. Reason., 1999

1993

Checking Algorithms for Pure Type Systems.

L. S. van Benthem Jutting, James McKinna, Robert Pollack

Proceedings of the Types for Proofs and Programs, 1993

Pure Type Systems Formalized.

James McKinna, Robert Pollack

Proceedings of the Typed Lambda Calculi and Applications, 1993

Deliverables: A Categorial Approach to Program Development in Type Theory.

James McKinna, Rod M. Burstall

Proceedings of the Mathematical Foundations of Computer Science 1993, 1993