Repository | Book | Chapter
(2006) Algebra, meaning, and computation, Dordrecht, Springer.
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.
Publication details
DOI: 10.1007/11780274_27
Full citation:
Goguen, H. , McBride, C. , McKinna, J. (2006)., Eliminating dependent pattern matching, in K. Futatsugi, J. Jouannaud & J. Meseguer (eds.), Algebra, meaning, and computation, Dordrecht, Springer, pp. 521-540.
This document is unfortunately not available for download at the moment.