default search action
James McKinna
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j11]Birthe van den Berg
, Tom Schrijvers
Forward- or reverse-mode automatic differentiation: What's the difference? Sci. Comput. Program. 231: 103010 (2024) - 2023
- [j10]Wenhao Tang
Structural Subtyping as Parametric Polymorphism. Proc. ACM Program. Lang. 7(OOPSLA2): 1093-1121 (2023) - [i7]Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley:
Structural Subtyping as Parametric Polymorphism. CoRR abs/2304.08267 (2023) - 2022
- [i6]Birthe van den Berg, Tom Schrijvers
Forward- or Reverse-Mode Automatic Differentiation: What's the Difference? CoRR abs/2212.11088 (2022) - 2021
- [j9]Guillaume Allais
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program. 31: e22 (2021) - 2020
- [e2]James McKinna, Cyrus Omar:
Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2020, Virtual Event, USA, August 23, 2020. ACM 2020, ISBN 978-1-4503-8051-5 [contents] - [i5]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 abs/2001.11001 (2020)
2010 – 2019
- 2019
- [j8]J. Garrett Morris
Abstracting extensible data types: or, rows by any other name. Proc. ACM Program. Lang. 3(POPL): 12:1-12:28 (2019) - 2018
- [j7]Guillaume Allais
A type and scope safe universe of syntaxes with binding: their semantics and proofs. Proc. ACM Program. Lang. 2(ICFP): 90:1-90:30 (2018) - [c33]Craig McLaughlin
Triangulating context lemmas. CPP 2018: 102-114 - 2017
- [j6]Faris Abou-Saleh, James McKinna, Jeremy Gibbons:
Coalgebraic Aspects of Bidirectional Computation. J. Object Technol. 16(1): 1:1-29 (2017) - [j5]James Cheney
On principles of Least Change and Least Surprise for bidirectional transformations. J. Object Technol. 16(1): 3:1-31 (2017) - [c32]Guillaume Allais
Type-and-scope safe programs and their proofs. CPP 2017: 195-207 - 2016
- [c31]Faris Abou-Saleh, James Cheney
Introduction to Bidirectional Transformations. Bidirectional Transformations 2016: 1-28 - [c30]Faris Abou-Saleh, James Cheney
Reflections on Monadic Lenses. A List of Successes That Can Change the World 2016: 1-31 - [c29]James McKinna:
Bidirectional Transformations with Deltas: A Dependently Typed Approach (Talk Proposal). Bx@ETAPS 2016: 14 - [c28]James McKinna, Perdita Stevens:
How to Regain Equilibrium without Losing your Balance? Scenarios for Bx Deployment (Discussion Paper). Bx@ETAPS 2016: 32-34 - [c27]James McKinna:
Complements Witness Consistency. Bx@ETAPS 2016: 90-94 - [i4]Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens:
Reflections on Monadic Lenses. CoRR abs/1601.02484 (2016) - 2015
- [c26]Faris Abou-Saleh, James Cheney
Notions of Bidirectional Computation and Entangled State Monads. MPC 2015: 187-214 - [c25]Faris Abou-Saleh, James McKinna, Jeremy Gibbons:
Coalgebraic Aspects of Bidirectional Computation. Bx@STAF 2015: 16-30 - [c24]James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens:
Towards a Principle of Least Surprise for Bidirectional Transformations. Bx@STAF 2015: 66-80 - [i3]Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens:
Notions of bidirectional computation and entangled state monads. CoRR abs/1505.02579 (2015) - 2014
- [c23]James Cheney, James McKinna, Perdita Stevens, Jeremy Gibbons:
Towards a Repository of Bx Examples. EDBT/ICDT Workshops 2014: 87-91 - [c22]James Cheney, James McKinna, Perdita Stevens, Jeremy Gibbons, Faris Abou-Saleh:
Entangled State Monads. EDBT/ICDT Workshops 2014: 108-111 - 2013
- [j4]Herman Geuvers, Robbert Krebbers, James McKinna:
The λμT-calculus. Ann. Pure Appl. Log. 164(6): 676-701 (2013) - [c21]Roberto M. Amadio, Nicholas Ayache, François Bobot
Certified Complexity (CerCo). FOPARA 2013: 1-18 - 2012
- [i2]Herman Geuvers, Robbert Krebbers, James McKinna:
The lambda-mu-T-calculus. CoRR abs/1204.0347 (2012) - 2011
- [j3]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) - [c20]Carst Tankink, James McKinna:
Dynamic Proof Pages. MathWikis@ITP 2011: 45-48 - 2010
- [c19]Carst Tankink
Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus 2010: 440-454 - [c18]Adam Gundry, Conor McBride
Type Inference in Context. MSFP@ICFP 2010: 43-54 - [c17]Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk:
Pure Type Systems without Explicit Contexts. LFMTP 2010: 53-67 - [c16]Carst Tankink
Narrating Formal Proof (Work in Progress). UITP 2010: 71-83 - [i1]Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk:
Proviola: A Tool for Proof Re-animation. CoRR abs/1005.2672 (2010)
2000 – 2009
- 2009
- [c15]Saleem Bhatti, Edwin C. Brady, Kevin Hammond, James McKinna:
Domain Specific Languages (DSLs) for Network Protocols (Position Paper). ICDCS Workshops 2009: 208-213 - [c14]Lionel Elie Mamane, Herman Geuvers, James McKinna:
A Logically Saturated Extension of lambdaµµ. Calculemus/MKM 2009: 405-421 - 2008
- [c13]Peter Chapman, James McKinna, Christian Urban:
Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. AISC/MKM/Calculemus 2008: 38-52 - [c12]Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers:
A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki 2008 - [c11]Eelis van der Weegen, James McKinna:
A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. TYPES 2008: 256-271 - 2007
- [c10]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: 159-176 - 2006
- [c9]Healfdene Goguen, Conor McBride, James McKinna:
Eliminating Dependent Pattern Matching. Essays Dedicated to Joseph A. Goguen 2006: 521-540 - [c8]Stéphane Lengrand, Roy Dyckhoff, James McKinna:
A Sequent Calculus for Type Theory. CSL 2006: 441-455 - [c7]James McKinna:
Why dependent types matter. POPL 2006: 1 - 2004
- [j2]Conor McBride, James McKinna:
The view from the left. J. Funct. Program. 14(1): 69-111 (2004) - [c6]Conor McBride, James McKinna:
Functional pearl: i am not a number-i am a free variable. Haskell 2004: 1-9 - [c5]Conor McBride, Healfdene Goguen, James McKinna:
A Few Constructions on Constructors. TYPES 2004: 186-200 - 2003
- [c4]Edwin C. Brady, Conor McBride, James McKinna:
Inductive Families Need Not Store Their Indices. TYPES 2003: 115-129 - 2002
- [e1]Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack:
Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers. Lecture Notes in Computer Science 2277, Springer 2002, ISBN 3-540-43287-6 [contents]
1990 – 1999
- 1999
- [j1]James McKinna, Robert Pollack:
Some Lambda Calculus and Type Theory Formalized. J. Autom. Reason. 23(3-4): 373-409 (1999) - 1993
- [c3]James McKinna, Rod M. Burstall:
Deliverables: A Categorial Approach to Program Development in Type Theory. MFCS 1993: 32-67 - [c2]James McKinna, Robert Pollack:
Pure Type Systems Formalized. TLCA 1993: 289-305 - [c1]L. S. van Benthem Jutting, James McKinna, Robert Pollack:
Checking Algorithms for Pure Type Systems. TYPES 1993: 19-61
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 23:16 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: