Semantic models

Small-step operational semantics is the most commonly employed formalism for proving type soundness of statically typed programming languages, because of its ability to distinguish stuck from non-terminating computations, as opposed to big-step operational semantics.

Despite this, big-step operational semantics is more abstract, and more useful for specifying interpreters.

In previous work we have proposed a new proof technique to prove type soundness of a Java-like language expressed in terms of its big-step operational semantics. However the presented proof is rather involved, since it requires showing that the set of proof trees defining the semantic judgment forms a complete metric space when equipped with a specific distance function. In this paper we propose a more direct and abstract approach that exploits a standard and general compactness property of the metric space of values, that allows approximation of the coinductive big-step semantics in terms of the small-step one; in this way type soundness can be proved by standard mathematical induction.

It is well known that big-step operational semantics are not suitable for proving soundness of type systems, because of their inability to distinguish stuck from non-terminating computations. We show how this problem can be solved by interpreting coinductively the rules for the standard big-step operational semantics of a Java-like language, thus making the claim of soundness more intuitive: whenever a program is well-typed, its coinductive operational semantics returns a value. Indeed, coinduction allows non-terminating computations to return values; this is proved by showing that the set of proof trees defining the semantic judgment forms a complete metric space when equipped with a proper distance function. In this way, we are able to prove soundness of a nominal type system w.r.t. the coinductive semantics. Since the coinductive semantics is sound w.r.t. the usual small-step operational semantics, the standard claim of soundness can be easily deduced.

We define a coinductive semantics for a simple Java-like language by simply interpreting coinductively the rules of a standard big-step operational semantics. We prove that such a semantics is sound w.r.t. the usual small-step operational semantics, and then prove soundness of a conventional nominal type system w.r.t. the coinductive semantics. From these two results, soundness of the type system w.r.t. the small-step semantics can be easily deduced. This new proposed approach not only opens up new possibilities for proving type soundness, but also provides useful insights on the connection between coinductive big-step operational semantics and type systems.

We present a simple parametric calculus of processes which exchange open mobile code, that is, code which may contain free variables to be bound by the receiver's code. Type safety is ensured by a combination of static and dynamic checks. That is, internal consistency of each process is statically verified, by relying on local type assumptions on missing code; then, when code is sent from a process to another, a runtime check based on a subtyping relation ensures that it can be successfully received, without requiring re-inspection of the code. In order to refuse communication in as few cases as possible, the runtime check accepts even mobile code which would be rejected if statically available, by automatically inserting coercions driven by the subtyping relation, as in the so-called Penn translation. The calculus is parametric in some ingredients which can vary depending on the specific language or system. Notably, we abstract away from the specific nature of the code to be exchanged, and of the static and dynamic checks. We formalize the notion of type safety in our general framework and provide sufficient conditions on the above ingredients which guarantee this property. We illustrate our approach on a simple lambda-calculus with records, where type safe exchange of mobile code is made problematic by conflicts due to components which were not explicitly required. In particular, we show that the standard coercion semantics given in the literature, with other aims, for this calculus, allows to detect and eliminate conflicts due to inner components, thus solving a problem which was left open in previous work on type-safe exchange of mobile code.

Mixins are modules which may contain deferred components, i.e. components not defined in the module itself; moreover, in contrast to parameterized modules (like ML functors), they can be mutually dependent and allow their definitions to be overridden. In a preceding paper we have defined syntax and denotational semantics of a kernel language of mixin modules. Here, we take instead an axiomatic approach, giving a set of algebraic laws expressing the expected properties of a small set of primitive operators on mixins. Interpreting axioms as rewriting rules, we get a reduction semantics for the language and prove the existence of normal forms. Moreover, we show that the model defined in the earlier paper satisfies the given axiomatization.

We define an extension of CASL, the standard language for algebraic specification, with a late binding mechanism. More precisely, we introduce a special kind of functions called methods, for which, differently to what happens for usual functions, overloading resolution is delayed at evaluation time and not required to be conservative. The extension consists, at the semantic level, in the definition of an institution LB supporting late binding which is defined on top of the standard subsorted institution of CASL and, at the linguistic level, in the enrichment of the CASL language with appropriate constructs for dealing with methods.

We define the language of mixin modules MIX(FL) with the aim of providing foundations for the design of module systems supporting mixins. Several working examples are presented showing the benefits of the use of mixins and overriding in module systems. The language is strongly typed and supports separate compilation. The denotational semantics of the language is based on an algebraic approach and is parametric in the semantics of the underlying core language. Hence, even though the language is defined on top of a specific core language, other kinds of core languages could be considered as well.

We define a specification formalism (formally, an institution) which provides a notion of dynamic type (the type which is associated to a term by a particular evaluation) and late binding (the fact that the function version to be invoked in a function application depends on the dynamic type of one or more arguments). Hence, it constitutes a natural formal framework for modeling object-oriented and other dynamically-typed languages and a basis for adding to them a specification level. In this respect, the main novelty is the capability of writing axioms related to a given type which are not required to hold for subtypes, hence can be “overridden” in further refinements, thus lifting at the specification level the possibility of reusing code which is offered by the object-oriented approach.

We address the problem of defining an algebraic framework for modularization supporting separate type-checking. In order to do that we introduce the notions of abstract type system and logic of constraints and we present a canonical construction of a model part, on top of a logic of constraints. This canonical construction works under reasonable assumptions on the underlying type system (e.g., soundness of the system). We show that the framework is suitable for defining the static and dynamic semantics of module languages, by giving a concrete example of construction on top of the type system of a simple typed module language. As a result, the subtyping relation between module interfaces is captured in a natural way by the notion of signature morphism.

Mixins are modules in which some components are deferred, i.e. their definition has to be provided by another module. Moreover, differently from parameterized modules (like ML functors), mixin modules can be mutually dependent and their composition supports redefinition of components (overriding). In this paper, we present a formal model of mixins and their basic composition operators. These operators can be viewed as a kernel language with clean semantics in which to express more complex operators of existing modular languages, including variants of inheritance in object oriented programming. Our formal model is given in an "institution independent" way, i.e. is parameterized by the semantic framework modeling the underlying core language.

We propose a new way of handling imperative features in the algebraic approach to composition of software modules, meant in its abstract categorical formulation. The basic idea is to consider, instead of a global state, orthogonal to the modular structure, the local state of a module as the collection of those components which have no associated definition but an extension which may vary dynamically. Following this intuition, composition of modules via classical operators like merge, renaming and hiding involves composition of the corresponding states, allowing one to give a truly compositional semantics of module languages. Thanks to the abstract categorical formulation, we are able to define a canonical construction of a framework for modules with state starting from a framework with no imperative features. This provides the theoretical basis for designing languages of modules with state in a way independent of the underlying core language.

In this thesis we present two formal frameworks for modeling modular languages. Following a modular approach, we separate the module and the core level of a modular language. On the linguistic side, this corresponds to define a kernel module language parametric in the underlying core language. On the semantic side, this corresponds to build a model part (in the sense of institutions), on top of a standard module framework. The standard module framework is a model part, too, satisfying some additional properties and intended as the formal counterpart of the core language. The first formal framework we propose deals with the notion of state, an essential component of modules in imperative languages. The second one is concerned with a notion of module, called mixin, which includes those of generic module and abstract class. In both cases, we present two canonical constructions yielding a formal framework where models denote modules with state and mixins, respectively, and we define a set of primitive operations over them.

Mixins are modules which may contain deferred components, i.e. components not defined in the module itself, and allow definitions to be overridden. We give an axiomatic definition of a set of operations for mixin combination, corresponding to a variety of constructs existing in programming languages (merge, hiding, overriding, functional composition, ...). In particular, we show that they can all be expressed in terms of three primitive operations (namely, sum, reduct and freeze), which are characterized by a small set of axioms. We show that the given axiomatization is sound w.r.t. to a model provided in some preceding work. Finally, we prove the existence of anormal form for mixin expressions.

We show that many different overriding operators present in programming languages can be expressed, adopting a mixin-based framework, in terms of three basic operators. In particular we propose two orthogonal classifications: strong (the overridden definition is canceled) or weak (the overridden definition still remains significant, as in Smalltalk's super feature), and preferential (priority to one of the two arguments) or general. We formalize the relation between all these versions. Our analysis and results are not bound to a particular language, since they are formulated within an algebraic framework for mixin modules which can be instantiated over different core languages.

We present an algebraic formalization of the notion of mixin module, i.e. a module where the definition of some components is deferred. Moreover, we define a set of basic operators for composing mixin modules, intended to be a kernel language with clean semantics in which to express more complex operators of existing modular languages, including variants of inheritance in object oriented programming. The semantics of the operators is given in an institution independent way, i.e. is parameterized on the semantic framework modeling features of the underlying core language.

We present a module algebra interpreted in the model of dynamic data-types. A data-type with state, or dynamic data type, is a data type in which the interpretation of operation symbols is depending on the internal state, which may change during the time. We formalize the above notion by a new mathematical structure, called object structure. From the point of view of programming languages, an object structure is the overall semantic value (the denotation) of a software module in an imperative context: Ada packages, Modula-2 modules and objects of object based languages can be thought as syntactic counterparts of object structures. Thus a first result of our approach is an abstract and natural definition of the semantic value of a whole module. A further result that we want to achieve is this semantics to be truly compositional, i.e. operations of composing modules to be interpreted as operations of object structures at the semantic level. We illustrate that by giving syntax and semantics of a module language which is parametric in the concrete syntax used for defining methods and components of the state. The introduction of state makes necessary to review the semantics of classical operators as given in a standard algebraic setting. In particular, we introduce a distinction between the visible and the internal signature of an object structure, which is essential for defining a reduct operation, hence for modelling export/hiding operators. Composition of visible signatures must be propagated to internal signatures in order to keep unchanged hidden components modulo renaming; this corresponds to consider co-products of particular diagrams in the category of signatures.

We address the problem of providing a rigorous formal model for classes of objects and the variety of inheritance relations. Classes are modelled by a new structure, called d-oid, which corresponds to see objects as data with state. The approach we take is a rather abstract one and so we model representation independent configurations of an object system by algebras, object identities by so called tracking map, and method calls as transformations of algebras. Seeing classes as d-oids allows us to define a hierarchy of inheritance relations, modelled by relations between d-oids and corresponding to different liberty levels in redefining methods. The classification we present distinguish essentially three levels of inheritance: minimal, regular and conservative.