Logic in Computer Science (LICS 1999)

Paper: Pattern Matching as Cut Elimination (at LICS 1999)

Authors: Serenella Cerrito Delia Kesner

Abstract

We present a typed pattern calculus with explicit pattern matching and explicit substitutions, where both the typing rules and the reduction rules are modeled on the same logical proof system, namely Gentzen sequent calculus for minimal logic. Our calculus is inspired by the Curry-Howard Isomorphism, in the sense that types, both for patterns and terms, correspond to propositions, terms correspond to proofs, and term reduction corresponds to sequent proof normalization performed by cut elimination. The calculus enjoys subject reduction, confluence, preservation of strong normalization w.r.t a system with meta-level substitutions and strong normalization for well-typed terms. As a consequence, it can be seen as an implementation calculus for functional formalisms defined with meta-level operations for pattern matching and substitutions.

BibTeX

  @InProceedings{CerritoKesner-PatternMatchingasCu,
    author = 	 {Serenella Cerrito and Delia Kesner},
    title = 	 {Pattern Matching as Cut Elimination},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {98--108},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }