@inbook{b0386032ed334379bcfc6ae225d7f834,
title = "Eliminating Dependent Pattern Matching",
abstract = "This paper gives a reduction-preserving translation from Coquand{\textquoteright}s dependent pattern matching [4] into a traditional type theory [11] with universes, inductive types and relations and the axiom K [22]. This translation serves as a proof of termination for structurally recursive pattern matching programs, provides an implementable compilation technique in the style of functional programming languages, and demonstrates the equivalence with a more easily understood type theory.",
author = "Healfdene Goguen and Conor McBride and James McKinna",
year = "2006",
doi = "10.1007/11780274_27",
language = "English",
isbn = "9783540354628",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "521--540",
booktitle = "Algebra, Meaning, and Computation",
}