Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming
ABSTRACT:
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 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.
AUTHORS: R.N.S. Rowe and S.J. van Bakel
WHEN: Thusday, January 28th, 2011, 13:00
WHERE: Sala Congressi EDISU
DATE-TAG:2011
- Individual Seminars (IS)