A META-LANGUAGE FOR TYPED OBJECT-ORIENTED LANGUAGES

In [12] we defined the lambda&-calculus, a simple extension of the typ ed lambda-calculus to model typed object-oriented languages. This pape r is the continuation or, rather, the companion of [12] since it analy zes the practical counterpart of the theoretical issues introduced the re. Indeed, to develop a formal study of type systems for object-orien ted languages we define a meta-language based on lambda& and we show, by a practical example, how it can be used to prove properties of a la nguage. 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 lang uage and a theorem on the translation of well-typed programs proves th e correctness of the type-checker of the toy language. As an aside we also illustrate the expressivity of the lambda&-based model by showing how to translate existing features like multiple inheritance and mult iple dispatch, but also by integrating in the toy language new feature s directly suggested by the model, such as first-class messages, a gen eralization 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 receiv er (i.e. of a privileged argument to which the message is passed), a n otion that is absent in languages like CLOS.