Eliminating dependent pattern matching

Healfdene Goguen

Conor McBride

James McKinna

pp. 521-540

in: Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer (eds), Algebra, meaning, and computation, Berlin, Springer, 2006

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.