12 citations · 13 across the 5 of their papers we have counts for
5 papers
Categorical Models of Amortized Cost: An Adjoint Relationship between Cost and Potential
David Binder, David Corfield, Dominic Orchard +1
Various type systems have been developed to track the cost of a computation using a cost-tracking monad . On its own, this only tracks the worst-case cost of a computati…
Grokking the Sequent Calculus (Functional Pearl)
David Binder, Marco Tzschentke, Marius Müller +1
The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The λμμ-calculus is a term assignment system for the sequent calculu…
Deriving Dependently-Typed OOP from First Principles -- Extended Version with Additional Appendices
David Binder, Ingo Skupin, Tim Süberkrüb +1
The expression problem describes how most types can easily be extended with new ways to produce the type or new ways to consume the type, but not both. When abstract syntax trees a…
Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference
Ishan Bhanuka, Lionel Parreaux, David Binder +1
Creating good type error messages for constraint-based type inference systems is difficult. Typical type error messages reflect implementation details of the underlying constraint-…
Data-Codata Symmetry and its Interaction with Evaluation Order
David Binder, Julian Jabs, Ingo Skupin +1
Data types and codata types are, as the names suggest, often seen as duals of each other. However, most programming languages do not support both of them in their full generality,…