Logic in Computer Science (LICS 2001)

Paper: Normalization by Evaluation for Typed Lambda Calculus with Coproducts (at LICS 2001)

Authors: Thorsten Altenkirch Peter Dybjer Martin Hofmann Philip Scott

Abstract

We solve the decision problem for simply typed lambda calculus with strong binary sums, equivalently the word problem for free cartesian closed categories with binary coproducts. Our method is based on the semantical technique known as "normalization by evaluation" and involves inverting the interpretation of the syntax into a suitable sheaf model and from this extracting appropriate unique normal forms. There is no rewriting theory involved, and the proof is completely constructive, allowing program extraction from the proof.

BibTeX

  @InProceedings{AltenkirchDybjerHof-NormalizationbyEval,
    author = 	 {Thorsten Altenkirch and Peter Dybjer and Martin Hofmann and Philip Scott},
    title = 	 {Normalization by Evaluation for Typed Lambda Calculus with Coproducts},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2001},
    year =	 2001,
    editor =	 {Joseph Halpern},
    month =	 {June}, 
    pages =      {303--310},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }