Skip to main content
SpringerLink
Log in

Characterizing Convergent Terms in Object Calculi via Intersection Types

  • Conference paper
  • First Online:
Typed Lambda Calculi and Applications (TLCA 2001)

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

Included in the following conference series:

Abstract

We give a simple characterization of convergent terms in Abadi and Cardelli untyped Object Calculus (\( \varsigma \) -calculus) via intersection types. We consider a λ-calculus with records and its intersection type assignment system. We prove that convergent λ-terms are characterized by their types. The characterization is then inherited by the object calculus via self-application interpretation.

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. M. Abadi, L. Cardelli, A Theory of Objects, Springer 1996.

    Google Scholar 

  2. M. Abadi, L. Cardelli, R. Viswanathan, “An interpretation of objects and object types” Proc. of of POPL’96 1996, 396–409.

    Google Scholar 

  3. S. Abramsky, “Domain Theory in Logical Form”, APAL 51, 1991, 1–77.

    MATH  MathSciNet  Google Scholar 

  4. S. Abramsky, C.-H. L. Ong “Full abstraction in the lazy lambda calculus”, Inf. Comput. 105(2), 1993, 159–267.

    Article  MATH  MathSciNet  Google Scholar 

  5. S. van Bakel, Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting, Ph.D. Thesis, Mathematisch Centrum, Amsterdam 1993.

    Google Scholar 

  6. H.P. Barendregt, M. Coppo, M. Dezani, “A Filter Lambda Model and the Completeness of Type Assignment”, JSL 48, 1983, 931–940.

    Article  MATH  Google Scholar 

  7. G. Boudol, “A Lambda Calculus for (Strict) Parallel Functions”, Info. Comp. 108, 1994, 51–127.

    Article  MATH  MathSciNet  Google Scholar 

  8. K.B. Bruce, “A paradigmatic Object-Oriented design, static typing and semantics”, J. of Fun. Prog. 1(4), 1994, 127–206.

    Article  MathSciNet  Google Scholar 

  9. K.B. Bruce, L. Cardelli, B.C. Pierce, “Comparing object encodings”, Proc. of TACS’97, LNCS 1281, 1997, 415–438.

    Google Scholar 

  10. K. Crary, “Simple, Efficient Object Encoding using Intersection Types”, CMU Technical Report CMU-CS-99-100.

    Google Scholar 

  11. M. Coppo, F. Damiani, P. Giannini, “Inference based analyses of functional programs: dead-code and strictness”, in M. Okada, M. Dezani eds., Theories of Types and Proofs, Mathematical Society of Japan, vol. 2, 1998 [28]}, 143–176.

    Google Scholar 

  12. M. Coppo, M. Dezani, B. Venneri, “Functional characters of solvable terms”, Grund. der Math., 27, 1981, 45–58.

    Article  MATH  Google Scholar 

  13. M. Coppo, A. Ferrari, “Type inference, abstract interpretation and strictness analysis”, TCS 121, 1993, 113–144.

    Article  MATH  MathSciNet  Google Scholar 

  14. M. Dezani, E. Giovannetti, U. de Liguoro, “Intersection types, λ-models and Böhm trees”, in M. Okada, M. Dezani eds., Theories of Types and Proofs, Mathematical Society of Japan, vol. 2, 1998 [28]}, 45–97.

    Google Scholar 

  15. M. Dezani, F. Honsell, Y. Motohama, “Compositional Characterizations of λ-terms using Intersection Types”, Proc. of MFCS’00, LNCS 1893, 2000, 304–313.

    Google Scholar 

  16. M. Dezani, U. de Liguoro, A. Piperno. “A filter model for concurrent lambda-calculus”, Siam J. Comput. 27(5), 1998, 1376–1419.

    Article  MATH  MathSciNet  Google Scholar 

  17. L. Egidi, F. Honsell, S. Ronchi della Rocca, “Operational, denotational and logical descriptions: a case study”, Fund. Inf. 16, 1992, 149–169.

    MATH  Google Scholar 

  18. K. Fisher, F. Honsell, J.C. Mitchell, “A lambda calculus of objects and method specialization”, Nordic J. Comput. 1, 1994, 3–37.

    MATH  MathSciNet  Google Scholar 

  19. A. Gordon, G. Rees, “Bisimilarity for first-order calculus of objects with subtyping”, Proc. of POPL’96, 1996, 386–395.

    Google Scholar 

  20. H. Ishihara, T. Kurata, “Completeness of intersection and union type assignment systems for call-by-value λ-models”, to appear in TCS.

    Google Scholar 

  21. S. Kamin, “Inheritance in Smalltalk-80: a denotational definition”, Proc. of POPL’88, 1988, 80–87.

    Google Scholar 

  22. J.L. Krivine, Lambda-calcul, types et modéles, Masson 1990.

    Google Scholar 

  23. J.C. Mitchell, Foundations for Programming Languages, MIT Press, 1996.

    Google Scholar 

  24. B. Pierce, Programming with Intersection Types and Bounded Polymorphism, Ph.D. Thesis, 1991.

    Google Scholar 

  25. G. Pottinger, “A Type Assignment System for Strongly Normalizable λ-terms”, in R. Hindley, J. Seldin eds., To H.B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalisms, Academic Press, 1980, 561–527.

    Google Scholar 

  26. J. Reynolds, “The Coherence of Languages with Intersection Types”, LNCS 526, 1991, 675–700.

    MathSciNet  Google Scholar 

  27. D. Scott, “Data types as lattices”, SIAM J. Comput. 5,n. 3, 1976, 522–587.

    Article  MATH  MathSciNet  Google Scholar 

  28. M. Takahashi, M. Okada, M. Dezani eds., Theories of Types and Proofs, Mathematical Society of Japan, vol. 2, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Ugo de’Liguoro

Authors
  1. Ugo de’Liguoro
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, USA

    Samson Abramsky

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de’Liguoro, U. (2001). Characterizing Convergent Terms in Object Calculi via Intersection Types. In: Abramsky, S. (eds) Typed Lambda Calculi and Applications. TLCA 2001. Lecture Notes in Computer Science, vol 2044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45413-6_25

Download citation

  • DOI: https://doi.org/10.1007/3-540-45413-6_25

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41960-0

  • Online ISBN: 978-3-540-45413-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation