Title :
Reduction-free normalisation for a polymorphic system
Author :
Altenkirch, Thorsten ; Hofmann, Martin ; Streicher, Thomas
Author_Institution :
Inst. fur Inf., Ludwig-Maximilians-Univ., Munchen, Germany
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
Keywords :
lambda calculus; programming theory; type theory; calculus; combinator version; impredicative constructive type theory; internal language; polymorphic system; presheaves; reduction-free normalisation; semantical proof; Calculus; Context modeling; Frequency shift keying; Reactive power;
Conference_Titel :
Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Conference_Location :
New Brunswick, NJ
Print_ISBN :
0-8186-7463-6
DOI :
10.1109/LICS.1996.561309
