Logic in Computer Science (LICS 1993)

Paper: A typed pattern calculus (at LICS 1993)

Authors: Val Breazu-Tannen Delia Kesner Laurence Puel

Abstract

The theory of programming with pattern-matching function definitions has been studied mainly in the framework of first-order rewrite systems. The authors present a typed functional calculus that emphasizes the strong connection between the structure of whole pattern definitions and their types. In this calculus, type-checking guarantees the absence of runtime errors caused by nonexhaustive pattern-matching definitions. Its operational semantics is deterministic in a natural way, without the imposition of ad hoc solutions such as clause order or best fit. The calculus is designed as a computational interpretation of the Gentzen sequent proofs for the intuitionistic propositional logic. The basic properties connecting typing and evaluation, subject reduction, and strong normalization are proved. The authors believe that this calculus offers a rational reconstruction of the pattern-matching features found in successful functional languages

BibTeX

  @InProceedings{BreazuTannenKesnerP-Atypedpatterncalcul,
    author = 	 {Val Breazu-Tannen and Delia Kesner and Laurence Puel},
    title = 	 {A typed pattern calculus},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {262--274},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }