@inproceedings{96822c54e61f4c92abfe8b836aaa0384,
title = "A few constructions on constructors",
abstract = "We present four constructions for standard equipment which can be generated for every inductive datatype: case analysis, structural recursion, no confusion, acyclicity. Our constructions follow a two-level approach-they require less work than the standard techniques which inspired them [11, 8]. Moreover, given a suitably heterogeneous notion of equality, they extend without difficulty to inductive families of datatypes. These constructions are vital components of the translation from dependently typed programs in pattern matching style [7] to the equivalent programs expressed in terms of induction principles [21] and as such play a crucial behind-the-scenes r (o) over cap le in Epigram [25].",
author = "C McBride and H Goguen and J McKinna",
year = "2006",
doi = "10.1007/11617990",
language = "English",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
pages = "186--200",
booktitle = "Types for Proofs and Programs",
address = "Germany",
}