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 lambda terms in normal form, normalizing, solvable and unsolvable terms. Hence, its application in the proof of the Genericity Lemma turns out to be appropriate.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Bakel, S. van (1992), Complete restrictions of the intersection type disciplines, Theoretical Computer Science 102, pp 136–163.
Barendregt, H.P. (1984), The Lambda Calculus — Its Syntax and Semantics, 2nd edition, North-Holland, Amsterdam.
Barendregt, H.P. (1992), Lambda calculi with types, in Handbook of Logic in Computer Science, S. Abramsky, D.M. Gabbay and T.S.E. Maibaum eds, Oxford University Press, Oxford, pp 117–309.
Barendregt, H.P., M. Coppo and M. Dezani-Ciancaglini (1983), A filter model and the completeness of type assignment, The Journal of Symbolic Logic 48(4), pp 931–940.
Coppo, M., M. Dezani-Ciancaglini, and B. Venneri (1980), Principal type schemes and λ-calculus semantics, in To H.B. Curry: Essays on Combinatory Logic, Typed Lambda Calculus and Formalism, J.R. Hindley and J.P. Seldin, eds, Academic Press, New York, pp 480–490.
Ghilezan, S. (1993), Intersection types in lambda calculus and logic, Ph. D. thesis, University of Novi Sad.
Krivine, J.L. (1990), Lambda-calcul types et modèls, Masson, Paris.
Ronchi della Roca, S. and B. Venneri (1984), Principal type schemes for an extended type theory, Theoretical Computer Science 28, pp 151–171.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ghilezan, S. (1994). Application of typed lambda calculi in the untyped lambda calculus. In: Nerode, A., Matiyasevich, Y.V. (eds) Logical Foundations of Computer Science. LFCS 1994. Lecture Notes in Computer Science, vol 813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58140-5_13
Download citation
DOI: https://doi.org/10.1007/3-540-58140-5_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58140-6
Online ISBN: 978-3-540-48442-4
eBook Packages: Springer Book Archive