Difunctorial Semantics of Object Calculus: Towards Algebra of Objects

Abstrakt:

I will give an introduction to Abadi and Cardelli's object calculus, a typed system similar to simply typed lambda calculus but where objects, rather than functions, are the primitive syntactic entities. I give a denotational model for the first order object calculus (without subtyping) in the category pCpo of cpos and partial maps. The key novelty of this new model is its extensive use of recursively defined types, supporting self-application, to model objects. At a technical level, this entails using some sophisticated techniques such as Freyd's algebraic compactness to guarantee the existence of the denotations of the object types. The key feature/complexity is the mixed variance functors which are needed to model object types.

I will show that a canonical recursion operator is inherent in this semantics. This operator can be useful in object-oriented programming: both in algebraic/coalgebraic formal methods and in capturing recurring abstractions in actual programs. The usefulness of the operator is witnessed by giving a straightforward translation of algebraic datatypes into so called wrapper classes. The talk concludes by comparing with Abadi and Cardelli's per semantics and by discussing current and future work.

The work reported here is joint work with Neil Ghani at University of Leicester.