Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming

(Extended Abstract)
  • Reuben Rowe
  • Steffen Van Bakel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)CrossRefzbMATHGoogle Scholar
  2. 2.
    van Bakel, S.: Intersection Type Assignment Systems. TCS 151(2), 385–435 (1995)CrossRefzbMATHGoogle Scholar
  3. 3.
    van Bakel, S.: Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalising. NDJFL 45(1), 35–63 (2004)zbMATHGoogle Scholar
  4. 4.
    van Bakel, S.: Completeness and Partial Soundness Results for Intersection & Union Typing for λμ μ. APAL 161, 1400–1430 (2010)zbMATHGoogle Scholar
  5. 5.
    van Bakel, S., de’Liguoro, U.: Logical equivalence for subtyping object and recursive types. ToCS 42(3), 306–348 (2008)zbMATHGoogle Scholar
  6. 6.
    van Bakel, S., Fernández, M.: Normalisation Results for Typeable Rewrite Systems. IaC 2(133), 73–116 (1997)zbMATHGoogle Scholar
  7. 7.
    van Bakel, S., Fernández, M.: Normalisation, Approximation, and Semantics for Combinator Systems. TCS 290, 975–1019 (2003)CrossRefzbMATHGoogle Scholar
  8. 8.
    van Bakel, S., Rowe, R.: Semantic Predicate Types for Class-based Object Oriented Programming. In: FTfJP 2009 (2009)Google Scholar
  9. 9.
    Banerjee, A., Jensen, T.P.: Modular Control-Flow Analysis with Rank 2 Intersection Types. MSCS 13(1), 87–124 (2003)zbMATHGoogle Scholar
  10. 10.
    Barendregt, H.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984)zbMATHGoogle Scholar
  11. 11.
    Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. JSL 48(4), 931–940 (1983)zbMATHGoogle Scholar
  12. 12.
    Cardelli, L., Mitchell, J.C.: Operations on Records. MSCS 1(1), 3–48 (1991)zbMATHGoogle Scholar
  13. 13.
    Cardelli, L.: A Semantics of Multiple Inheritance. IaC 76(2/3), 138–164 (1988)zbMATHGoogle Scholar
  14. 14.
    Coppo, M., Dezani-Ciancaglini, M.: An Extension of the Basic Functionality Theory for the λ-Calculus. NDJFL 21(4), 685–693 (1980)zbMATHGoogle Scholar
  15. 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)CrossRefzbMATHGoogle Scholar
  16. 16.
    Curry, H.B.: Grundlagen der Kombinatorischen Logik. AJM 52, 509–536, 789–834 (1930)zbMATHGoogle Scholar
  17. 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)CrossRefGoogle Scholar
  18. 18.
    Fisher, K., Honsell, F., Mitchell, J.C.: A lambda Calculus of Objects and Method Specialization. NJ 1(1), 3–37 (1994)zbMATHGoogle Scholar
  19. 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)CrossRefGoogle Scholar
  20. 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)CrossRefGoogle Scholar
  21. 21.
    Mitchell, J.C.: Type Systems for Programming Languages. In: Handbook of TCS, vol. B, ch. 8, pp. 415–431 (1990)Google Scholar
  22. 22.
    Nakano, H.: A Modality for Recursion. In: LICS, pp. 255–266 (2000)Google Scholar
  23. 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)CrossRefGoogle Scholar
  24. 24.
    Plotkin, G.D.: The origins of structural operational semantics. JLAP 60-61, 3–15 (2004)zbMATHGoogle Scholar
  25. 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)CrossRefGoogle Scholar
  26. 26.
    Tait, W.W.: Intensional interpretation of functionals of finite type I. JSL 32(2), 198–223 (1967)zbMATHGoogle Scholar
  27. 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)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Reuben Rowe
    • 1
  • Steffen Van Bakel
    • 1
  1. 1.Department of ComputingImperial College LondonLondonUK

Personalised recommendations