Skip to main content
SpringerLink
Log in

Two Behavioural Lambda Models

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 2002)

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

Included in the following conference series:

Abstract

We build two inverse limit lambda models which characterize completely sets of terms having similar computational behaviour. More precisely for each one of these sets of terms there is a corresponding element in at least one of the two models such that a term belongs to the set if and only if its interpretation (in a suitable environment) is greater than or equal to that element. This is proved by using the finitary logical description of the models obtained by defining suitable intersection type assignment systems.

Partially supported by EU within the FET — Global Computing initiative, project DART ST-2001-33477, and by MURST Cofin’01 project COMETA. The funding bodies are not responsible for any use that might be made of the results presented here.

Partially supported by grant 1630 “Representation of proofs with applications, classification of structures and infinite combinatorics” (of the Ministry of Science, Technology, and Development of Serbia).

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Samson Abramsky. Domain theory in logical form. Ann. Pure Appl. Logic, 51(1–2):1–77, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  2. Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Inform. and Comput., 105(2):159–267, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  3. Fabio Alessi. Strutture di tipi, teoria dei domini e modelli del lambda calcolo. PhD thesis, Torino University, 1991.

    Google Scholar 

  4. Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi. Cambridge University Press, Cambridge, 1998.

    MATH  Google Scholar 

  5. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symbolic Logic, 48(4):931–940 (1984), 1983.

    MathSciNet  Google Scholar 

  6. Henk P. Barendregt. The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam, revised edition, 1984.

    MATH  Google Scholar 

  7. Corrado Böhm and Mariangiola Dezani-Ciancaglini. λ-terms as total or partial functions on normal forms. In C. Böhm, editor, λ-calculus and Computer Science Theory, volume 37 of Lecture Notes in Computer Science, pages 96–121, Berlin, 1975. Springer.

    Chapter  Google Scholar 

  8. Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell, and Giuseppe Longo. Extended type structures and filter lambda models. In G. Lolli, G. Longo, and A. Marcja, editors, Logic colloquium’ 82, pages 241–262, Amsterdam, 1984. North-Holland.

    Google Scholar 

  9. Mariangiola Dezani-Ciancaglini and Silvia Ghilezan. A lambda model characterizing computational behaviours of terms. In Y. Toyama, editor, International Workshop on Rewriting in Proof and Computation, RPC’01, pages 100–119, 2001.

    Google Scholar 

  10. Mariangiola Dezani-Ciancaglini, Furio Honsell, and Yoko Motohama. Compositional characterization of λ-terms using intersection types. In Mathematical Foundations of Computer Science 2000, volume 1893 of Lecture Notes in Computer Science, pages 304–313. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  11. Jean Gallier. Typing untyped λ-terms, or reducibility strikes again! Ann. Pure Appl. Logic, 91:231–270, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  12. Silvia Ghilezan. Strong normalization and typability with intersection types. Notre Dame J. Formal Logic, 37(1):44–52, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  13. Jean-Yves Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’elimination des coupures dans l’analyse et la théorie des types. In J.E. Fenstadt, editor, 2nd Scandinavian Logic Symposium, pages 63–92. North-Holland, 1971.

    Google Scholar 

  14. Peter T. Johnstone. Stone Spaces. Cambridge University Press, Cambridge, 1986. Reprint of the 1982 edition.

    MATH  Google Scholar 

  15. George Koletsos. Church-Rosser theorem for typed functionals. Journal of Symbolic Logic, 50: 782–790, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  16. Jean-Louis Krivine. Lambda-calcul Types et modèles. Masson, Paris, 1990.

    MATH  Google Scholar 

  17. Jean-Louis Krivine. Lambda-calculus, types and models. Ellis Horwood, New York, 1993. Translated from the 1990 French original by René Cori.

    MATH  Google Scholar 

  18. Daniel Leivant. Typing and computational properties of lambda expressions. Theoret. Comput. Sci., 44(1):51–68, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  19. Per Martin-Löf. Lecture notes on domain interpretation of type theory. Programming Methodology Group, Workshop on the Semantics of Programming Languages, Chalmers University of Technology, 1983.

    Google Scholar 

  20. John C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 415–431. Elsevier, Amsterdam, 1990.

    Google Scholar 

  21. John C. Mitchell. Foundation for Programmimg Languages. MIT Press, 1996.

    Google Scholar 

  22. Gordon D. Plotkin. Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci., 121(1–2):351–409, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  23. Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. In J.P. Seldin and J.R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 561–577. Academic Press, London, 1980.

    Google Scholar 

  24. Dana S. Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97–136, Berlin, 1972. Springer.

    Google Scholar 

  25. Dana S. Scott. Open problem. In C. Böhm, editor, Lambda Calculus and Computer Science Theory, volume 37 of Lecture Notes in Computer Science, page 369. Springer, Berlin, 1975.

    Google Scholar 

  26. Dana S. Scott. Domains for denotational semantics. In M. Nielsen and E.M. Schmidt, editors, Automata, Languages and Programming, pages 577–613. Springer, Berlin, 1982.

    Chapter  Google Scholar 

  27. Richard Statman. Logical relations and the typed λ-calculus. Information and Control, 65: 85–97, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  28. William W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32:198–212, 1967.

    Article  MATH  MathSciNet  Google Scholar 

  29. William W. Tait. A realizability interpretation of the theory of species. In R. Parikh, editor, Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 240–251. Springer, 1975.

    Google Scholar 

  30. Steffen van Bakel. Complete restrictions of the intersection type discipline. Theoret. Comput. Sci., 102(1):135–163, 1992.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, Torino, Italy

    Mariangiola Dezani-Ciancaglini

  2. Faculty of Engineering, University of Novi Sad, Yugoslavia

    Silvia Ghilezan

Authors
  1. Mariangiola Dezani-Ciancaglini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Silvia Ghilezan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Nijmegen, Toernooiveld 1, 6525 ED, Nijmegen, The Netherlands

    Herman Geuvers  & Freek Wiedijk  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dezani-Ciancaglini, M., Ghilezan, S. (2003). Two Behavioural Lambda Models. In: Geuvers, H., Wiedijk, F. (eds) Types for Proofs and Programs. TYPES 2002. Lecture Notes in Computer Science, vol 2646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-39185-1_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-39185-1_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-14031-3

  • Online ISBN: 978-3-540-39185-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation