Lics

IEEE Symposium on Logic in Computer Science

Paper: Reduction-free normalisation for a polymorphic system (at LICS 1996)

Abstract

We give a semantical proof that every term of a combinator version of system F has a normal form. As the argument is entirely formalisable in an impredicative constructive type theory a reduction-free normalisation algorithm can be extracted from this. The proof is presented as the construction of a model of the calculus inside a category of presheaves. Its definition is given entirely in terms of the internal language.

BibTeX

 @InProceedings{AltenkirchHofmannSt-Reductionfreenormal,
 author = 	 {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
 title = 	 {Reduction-free normalisation for a polymorphic system},
 booktitle = {Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996)},
 year =	 {1996},
 month =	 {July}, 
 pages = {98--106},
 location = {New Brunswick, NJ, USA}, 
 publisher =	 {IEEE Computer Society Press}
 }