Design and foundations of modular and object-oriented languages and systems
(updated February 2003)
KEYWORDS
Language design,
Types,
Semantics,
Program modules,
Object-oriented paradigm,
Separate compilation and linking
This research topic is related to advanced linguistic mechanisms for
software reuse, with the aim of of both language analysis/design and
development of theoretical foundations.
ACTIVITIES
Design and foundations of module systems
We have developed a unifying linguistic and semantic framework for modular languages, based on the
now widely accepted principle of seeing a module language as a small
language of its own, with its typing and reduction rules, which can be instantiated in
principle on different core languages.
This framework allows to express,
using a small set of primitive operators with clean and simple semantics, a
variety of different mechanisms for module composition: parametric
modules like ML functors, mutually recursive modules, overriding mechanisms as in the object-oriented paradigm.
- In
[ALP96] (short version) and
[MSCS98] we
present semantic foundations of a notion of "mixin", meant as a
module where some components can be either "deferred", i.e.,
without an associated definition, or "virtual", i.e., their
definition can be changed in a way that propagates to the referring components,
as it happens for methods in the object-oriented approach. Mixin modules can be seen as functions
from models into models (in a given institution), generalizing the Cook's approach to
the semantics of inheritance.
- In
[WADT97] (short
version) and [MSCS02]
we give an axiomatization of the operators and a corresponding normal form theorem.
- In
[PLILP97] we show how to express by means of these
basic operators a variety of inheritance operators of object-oriented languages,
and in [AMAST00] and
[AGP00] we present concrete instances of our
mixin language using as core a simple functional language and a logic
language.
- A comprehensive presentation of a major part of the above described research
on mixin modules can be found in D. Ancona's
Ph.
D. thesis.
- In [PPDP99] (short
version) and [JFP02] we present a
primitive calculus of module systems (CMS) equipped with a
type system and reduction semantics. We prove confluence and type soundness
and show how to encode in CMS other basic calculi like lambda-calculus and
Abadi-Cardelli's object calculus.
Analysis and formalization of object-oriented languages
This activity concerns formalization of various features of
object-oriented languages (e.g., exception handling in presence of
inheritance) and design, formalization and implementation of
extensions of object-oriented languages with features which
enhance flexibility, as, e.g., mixin classes and dynamic object
re-classification
(collaboration with University of Torino and Imperial College, London).
- In [ECOOP00] we propose an extension of
Java with mixin classes (parametric heir classes).
- In [FTfJP00] we analyse the
Java
overloading resolution mechanism and propose an alternative rule.
- In [ECOOP01] we propose a true
module system on top of Java.
- In [OOPSLA01] we define a
simple calculus modeling Java checked exceptions.
- In [ICTCS01] and [ENTCS02] we define
translations from Fickle (an extension of Java supporting dynamic object
re-classification) into plain Java.
Formal frameworks for separate
compilation and linking
This activity concerns the development of formal frameworks allowing to
express separate compilation and linking as, e.g., in Java, and their
desired properties, and development of more flexible compilation
mechanisms guaranteeing safe linking at run-time and/or true
separate compilation
(collaboration with Imperial College, London).
- In [ECOOP02] we define a formal notion,
called compilation schema, allowing to specify different possibilities for performing the
overall process of Java compilation. We define a safe compilation schema for
this language and formally prove type safety.
- In [PPDP02] we define a type system
modeling true separate compilation for a small but significant Java subset, in the sense
that a single class declaration can be intra-checked (following the Cardelli's terminology)
and compiled providing a minimal set of type requirements on missing classes.
- In [ESOP03] we develop a non deterministic
model which includes the behaviour of Java and C-sharp dynamic linking
mechanisms. We also prove that all execution strategies are equivalent in
the sense that all terminating executions which do not involve a link error
give the same result.
Back to previous page
Please send suggestions and comments to:
Elena Zucca zucca@disi.unige.it
Last Updated: February 28, 2003
|