Home | Search | Help  
Home Page Università di Genova

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

PEOPLE

Elena Zucca
Associate professor
Davide Ancona
Assistant professor
Sonia Fagorzi
PhD Student
Giovanni Lagorio
PhD Student
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