Skip to main content
SpringerLink
Log in

Application of typed lambda calculi in the untyped lambda calculus

  • Conference paper
  • First Online:
Logical Foundations of Computer Science (LFCS 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 813))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bakel, S. van (1992), Complete restrictions of the intersection type disciplines, Theoretical Computer Science 102, pp 136–163.

    Google Scholar 

  2. Barendregt, H.P. (1984), The Lambda Calculus — Its Syntax and Semantics, 2nd edition, North-Holland, Amsterdam.

    Google Scholar 

  3. 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.

    Google Scholar 

  4. 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.

    Google Scholar 

  5. 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.

    Google Scholar 

  6. Ghilezan, S. (1993), Intersection types in lambda calculus and logic, Ph. D. thesis, University of Novi Sad.

    Google Scholar 

  7. Krivine, J.L. (1990), Lambda-calcul types et modèls, Masson, Paris.

    Google Scholar 

  8. Ronchi della Roca, S. and B. Venneri (1984), Principal type schemes for an extended type theory, Theoretical Computer Science 28, pp 151–171.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Engineering, University of Novi Sad, Trg Dositeja Obradovića 6, 21000, Novi Sad, Yugoslavia

    Silvia Ghilezan

Authors
  1. Silvia Ghilezan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Anil Nerode Yu. V. Matiyasevich

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation