25 citations · 33 across the 4 of their papers we have counts for
4 papers · 1 filter
Dependent Pearl: Normalization by realizability
Pierre-Évariste Dagand, Lionel Rieg, Gabriel Scherer
For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or pe…
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…