A meta-language for typed object-oriented languages

In [13] we defined the λ&-calculus, a simple extension of the typed λcalculus to model typed object-oriented languages. This paper is the continuation or, rather, the companion of [13] since it analyzes the practical counterpart of the theoretical issues introduced there. Indeed, to develop a formal study of type systems for object-oriented languages we define a meta-language based on λ& and we show, by a practical example, how it can be used it to prove properties of a language. To this purpose, we define a toy object-oriented language and its type-checking algorithm; then we translate this toy language into our meta-language. The translation gives the semantics of the toy language and a theorem on the translation of well-typed programs proves the correctness of the type-checker of the toy language. As an aside we also illustrate the expressivity of the λ&-based model by showing how to translate existing features like multiple inheritance and multiple dispatch, but also by integrating in the toy language new features directly suggested by the model, such as first-class messages, a generalization of the use of super and the use of explicit coercions. An important novelty with respect to previous systems is that we show how to model multiple dispatch also in the presence of a notion of receiver (i.e. of a privileged argument to which the message is passed), a notion that is absent in languages like CLOS.