DocumentCode
2721125
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
fYear
1996
fDate
27-30 Jul 1996
Firstpage
98
Lastpage
106
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Conference_Location
New Brunswick, NJ
ISSN
1043-6871
Print_ISBN
0-8186-7463-6
Type
conf
DOI
10.1109/LICS.1996.561309
Filename
561309
Link To Document