A framework for defining object-calculi

Abstract

In this paper, we give a general framework for the foundation of an operational (small step) semantics of object-based languages with an emphasis on functional and imperative issues. The framework allows classifying very naturally many object-based calculi according to their main implementation techniques of inheritance, namely delegation and embedding, and their particular strategies. This distinction comes easily from a choice in the rules. Our framework is founded on two previous works: λObj+,a versionof the Lambda Calculus of Objects of Fischer, Honsell, and Mitchell, for the object aspects, and λσaω of Benaissa, Lescanne, and Rose, for the description of the operational semantics and sharing. The former is the formalization of a small delegation-based language which contains both lambda calculus and object primitives to create, update, and send messages to objects, while the latter is designed to provide a generic description of functional language implementations and is based on a calculus of explicit substitution extended with addresses to deal with memory management. The framework is presented as a set of modules, each of which captures a particular aspect of object-calculi (functional vs. imperative, delegation vs. embedding, and any combination of them). Above all, it introduces and illustrates a new promising approach to formally reason about the operational semantics of languages with (possibly) mutable states.