Please use this identifier to cite or link to this item:
https://open.uns.ac.rs/handle/123456789/10031
Title: | Application of typed lambda calculi in the untyped lambda calculus | Authors: | Gilezan, Silvia | Issue Date: | 1-Jan-1994 | Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Abstract: | © 1994, Springer Verlag. All rights reserved. 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. | URI: | https://open.uns.ac.rs/handle/123456789/10031 | ISBN: | 9783540581406 | ISSN: | 3029743 |
Appears in Collections: | FTN Publikacije/Publications |
Show full item record
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.