@inproceedings{84b1d2f0c9144542a53ad7d504f24a0c,
title = "Eliminating dependent pattern matching",
abstract = "This paper gives a reduction-preserving translation from Coquand'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.",
keywords = "CALCULUS",
author = "Healfdene Goguen and Conor McBride and James McKinna",
year = "2006",
doi = "10.1007/11780274",
language = "English",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
pages = "521--540",
booktitle = "Algebra, Meaning and Computation",
address = "Germany",
}