| 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 | Abstract: | 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
SCOPUSTM
Citations
2
checked on Jul 24, 2024
Page view(s)
51
checked on May 9, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.