137 citations · 160 across the 8 of their papers we have counts for
8 papers
Structural Subtyping as Parametric Polymorphism
Wenhao Tang, Daniel Hillerström, James McKinna +4
Structural subtyping and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider rec…
Forward- or Reverse-Mode Automatic Differentiation: What's the Difference?
Birthe van den Berg, Tom Schrijvers, James McKinna +1
Automatic differentiation (AD) has been a topic of interest for researchers in many disciplines, with increased popularity since its application to machine learning and neural netw…
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
Guillaume Allais, Robert Atkey, James Chapman +2
Almost every programming language's syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of -equivalence, capture-avoiding…
Notions of bidirectional computation and entangled state monads
Faris Abou-Saleh, James Cheney, Jeremy Gibbons +2
Bidirectional transformations (bx) support principled consistency maintenance between data sources. Each data source corresponds to one perspective on a composite system, manifeste…
The lambda-mu-T-calculus
Herman Geuvers, Robbert Krebbers, James McKinna
Calculi with control operators have been studied as extensions of simple type theory. Real programming languages contain datatypes, so to really understand control operators, one s…
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
Stéphane Jean Eric Lengrand, Roy Dyckhoff, James McKinna
Basic proof-search tactics in logic and type theory can be seen as the root-first applications of rules in an appropriate sequent calculus, preferably without the redundancies gene…
Pure Type Systems without Explicit Contexts
Herman Geuvers, Robbert Krebbers, James McKinna +1
We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of shape "Gamma |- A : B", our systems just have judgments o…
Proviola: A Tool for Proof Re-animation
Carst Tankink, Herman Geuvers, James McKinna +1
To improve on existing models of interaction with a proof assistant (PA), in particular for storage and replay of proofs, we in- troduce three related concepts, those of: a proof m…