Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Sixteenth Annual IEEE Symposium on

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 J. 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 J. Scott},
    title = 	 {Normalization by Evaluation for Typed Lambda Calculus with Coproducts},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {303--310},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski