25 citations · 56 across the 6 of their papers we have counts for
5 papers · 1 filter
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…
New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized
Guillaume Allais, Pierre Boutillier, Conor McBride
The definitional equality of an intensional type theory is its test of type compatibility. Today's systems rely on ordinary evaluation semantics to compare expressions in types, fr…
A Categorical Treatment of Ornaments
Pierre-Evariste Dagand, Conor McBride
Ornaments aim at taming the multiplication of special-purpose datatype in dependently-typed theory. In its original form, the definition of ornaments is tied to a particular univer…
Elaborating Inductive Definitions
Pierre-Evariste Dagand, Conor McBride
We present an elaboration of inductive definitions down to a universe of datatypes. The universe of datatypes is an internal presentation of strictly positive families within type…
Transporting Functions across Ornaments
Dagand Pierre-Evariste, McBride Conor
Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of data-types: we can finally write correct-by-constr…