Skip to main content
SpringerLink
Log in
Book cover

International Conference on Typed Lambda Calculi and Applications

TLCA 2011: Typed Lambda Calculi and Applications pp 229–244Cite as

Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming

(Extended Abstract)

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6690))

Abstract

We consider a semantics for a class-based object-oriented calculus based upon approximation; since in the context of LC such a semantics enjoys a strong correspondence with intersection type assignment systems, we also define such a system for our calculus and show that it is sound and complete. We establish the link with between type (we use the terminology predicate here) assignment and the approximation semantics by showing an approximation result, which leads to a sufficient condition for head-normalisation and termination.

We show the expressivity of our predicate system by defining an encoding of Combinatory Logic (and so also LC) into our calculus. We show that this encoding preserves predicate-ability and also that our system characterises the normalising and strongly normalising terms for this encoding, demonstrating that the great analytic capabilities of these predicates can be applied to OO.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)

    Book  MATH  Google Scholar 

  2. van Bakel, S.: Intersection Type Assignment Systems. TCS 151(2), 385–435 (1995)

    Article  MATH  Google Scholar 

  3. van Bakel, S.: Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalising. NDJFL 45(1), 35–63 (2004)

    MATH  Google Scholar 

  4. van Bakel, S.: Completeness and Partial Soundness Results for Intersection & Union Typing for λμ μ. APAL 161, 1400–1430 (2010)

    MATH  Google Scholar 

  5. van Bakel, S., de’Liguoro, U.: Logical equivalence for subtyping object and recursive types. ToCS 42(3), 306–348 (2008)

    MATH  Google Scholar 

  6. van Bakel, S., Fernández, M.: Normalisation Results for Typeable Rewrite Systems. IaC 2(133), 73–116 (1997)

    MATH  Google Scholar 

  7. van Bakel, S., Fernández, M.: Normalisation, Approximation, and Semantics for Combinator Systems. TCS 290, 975–1019 (2003)

    Article  MATH  Google Scholar 

  8. van Bakel, S., Rowe, R.: Semantic Predicate Types for Class-based Object Oriented Programming. In: FTfJP 2009 (2009)

    Google Scholar 

  9. Banerjee, A., Jensen, T.P.: Modular Control-Flow Analysis with Rank 2 Intersection Types. MSCS 13(1), 87–124 (2003)

    MATH  Google Scholar 

  10. Barendregt, H.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984)

    MATH  Google Scholar 

  11. Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. JSL 48(4), 931–940 (1983)

    MATH  Google Scholar 

  12. Cardelli, L., Mitchell, J.C.: Operations on Records. MSCS 1(1), 3–48 (1991)

    MATH  Google Scholar 

  13. Cardelli, L.: A Semantics of Multiple Inheritance. IaC 76(2/3), 138–164 (1988)

    MATH  Google Scholar 

  14. Coppo, M., Dezani-Ciancaglini, M.: An Extension of the Basic Functionality Theory for the λ-Calculus. NDJFL 21(4), 685–693 (1980)

    MATH  Google Scholar 

  15. Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional characters of solvable terms. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 27, 45–58 (1981)

    Article  MATH  Google Scholar 

  16. Curry, H.B.: Grundlagen der Kombinatorischen Logik. AJM 52, 509–536, 789–834 (1930)

    MATH  Google Scholar 

  17. Damiani, F., Prost, F.: Detecting and Removing Dead-Code using Rank 2 Intersection. In: Giménez, E. (ed.) TYPES 1996. LNCS, vol. 1512, pp. 66–87. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  18. Fisher, K., Honsell, F., Mitchell, J.C.: A lambda Calculus of Objects and Method Specialization. NJ 1(1), 3–37 (1994)

    MATH  Google Scholar 

  19. Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001)

    Article  Google Scholar 

  20. Jensen, T.P.: Types in Program Analysis. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 204–222. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. Mitchell, J.C.: Type Systems for Programming Languages. In: Handbook of TCS, vol. B, ch. 8, pp. 415–431 (1990)

    Google Scholar 

  22. Nakano, H.: A Modality for Recursion. In: LICS, pp. 255–266 (2000)

    Google Scholar 

  23. Parigot, M.: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  24. Plotkin, G.D.: The origins of structural operational semantics. JLAP 60-61, 3–15 (2004)

    MATH  Google Scholar 

  25. Scott, D.: Domains for Denotational Semantics. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 577–613. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  26. Tait, W.W.: Intensional interpretation of functionals of finite type I. JSL 32(2), 198–223 (1967)

    MATH  Google Scholar 

  27. Wadsworth, C.P.: The relation between computational and denotational properties for Scott’s D ∞ -models of the lambda-calculus. SIAM J. Comput. 5, 488–521 (1976)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College London, 180 Queen’s Gate, London, SW7 2BZ, UK

    Reuben Rowe & Steffen Van Bakel

Authors
  1. Reuben Rowe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Steffen Van Bakel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

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

    Luke Ong

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rowe, R., Van Bakel, S. (2011). Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming. In: Ong, L. (eds) Typed Lambda Calculi and Applications. TLCA 2011. Lecture Notes in Computer Science, vol 6690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21691-6_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-21691-6_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-21690-9

  • Online ISBN: 978-3-642-21691-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation