We consider a semantics for a class-based object-oriented calculus based upon approximation; since in the context of Lambda Calculus 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 in turn 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 strongly normalising terms for this encoding, demonstrating that the great analytic capabilities of these predicates can be applied to OO.
This is joint work with R.N.S. Rowe.
The talk is aimed at a non-expert audience in either the topic of object oriented programming, approximation semantics, or intersection type assignment.