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. Dedicated to Professor Joseph Goguen on the occasion of his 65th birthday.

• Type: Conference
• Year: 2006
• Where: BIRTHDAY
• Authors: Healfdene Goguen, Conor McBride, James McKinna
• Keywords: Applied Computing, BIRTHDAY 2006, Coquand's Dependent Pattern, Pattern Matching, Type Theory