Authors: Ghilezan, Silvia 
Title: Application of typed lambda calculi in the untyped lambda calculus
Journal: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume: 813 LNCS
First page: 129
Last page: 139
Conference: 3rd International Symposium on Logical Foundations of Computer Science, LFCS 1994; St. Petersburg; Russian Federation; 11 July 1994 through 14 July 1994
Issue Date: 1-Jan-1994
Rank: M23
ISBN: 978-3-540-58140-6
ISSN: 0302-9743
DOI: 10.1007/3-540-58140-5_13
We discuss some properties of typed lambda calculi which can be related and applyed to the proofs of some properties of the untyped lambda calculus. The strong normalization property of the intersection type assignment system is used in order to prove the finitness of developments property of the untyped lambda calculus in Krivine (1990). Similarly, the strong normalization property of the simply typed lambda calculus can be used for the same reason. Typability in various intersection type assignment systems characterizes tambda terms in normal form, normalizing, solvable and unsolvable terms. Hence, its application in the proof of the Genericity Lemma turns out to be appropriate.
Publisher: Springer Link

Show full item record


checked on May 16, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.