This paper gives a reduction-preserving translation from Coquand’s dependent pattern matching  into a traditional type theory  with universes, inductive types and relations and the axiom K . 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.
|Title of host publication||Algebra, Meaning, and Computation|
|Number of pages||20|
|Publication status||Published - 2006|
|Name||Lecture Notes in Computer Science|