A meta-language for typed object-oriented languages

Abstract

In [3] we defined the λ&-calculus, a simple extension of the typed λ-calculus to model typed object-oriented languages. To develop a formal study of type systems for object-oriented languages we define, in this paper, a meta-language based on λ& and we show by a practical example how to use 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 correction 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.