25 citations · 56 across the 6 of their papers we have counts for
Showing 2012Show all
3 papers · 1 filter
cs.PL2012
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…
cs.PL2012★ 7 cited
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…
cs.PL2012★ 25 cited
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…