Papers available

Intersection types for unbind and rebind (extended abstract)

with M. Dezani, P. Giannini

Intersection Types and Related Systems (ITRS'10). To appear.

We define a type system with intersection types for an extension of lambda-calculus with unbind and rebind operators. In this calculus, a term t with free variables x₁, ..., x_n, representing open code, can be packed into an unbound term
<x₁, ..., x_n | t>, and passed around as a value. In order to execute inside code, an unbound term should be explicitly rebound at the point where it is used. Unbinding and rebinding are hierarchical, that is, the term t can contain arbitrarily nested unbound terms, whose inside code can only be executed after a sequence of rebinds has been applied. Correspondingly, types are decorated with levels, and a term has type τ^k if it needs k rebinds in order to reduce to a value of type τ. With intersection types we model the fact that a term can be used differently in contexts providing a different numbers of unbinds. In particular, top-level terms, that is, terms not requiring unbinds to reduce to values, should have a value type, that is, an intersection type where at least one element has shape τ⁰. With the proposed intersection type system we get soundness w.r.t the call-by-value strategy, an issue which was not resolved by previous type systems.

The paper is available at http://www.disi.unige.it/person/ZuccaE/Research/papers/ITRS10.pdf.

MetaFJig - A meta-circular composition language for Java-like classes

with M. Servetto

Technical report. March 2010. Submitted for publication.

We propose a Java-like language where class definitions are first class values and new classes can be derived from existing ones by exploiting the full power of the language itself, used on top of a small set of primitive composition operators, instead of using a fixed mechanism like inheritance.

Hence, compilation requires to perform {(meta-)reduction} steps, by a process that we call compile-time execution. This approach differs from meta-programming techniques available in mainstream languages since it is meta-circular, hence programmers are not required to learn new syntax and idioms.

Compile-time execution is guaranteed to be sound (not to get stuck) by a lightweight technique, where class composition errors are detected dynamically, and conventional typing errors are detected by interleaving typechecking with meta-reduction steps. This allows for a modular approach, that is, compile-time execution is defined, and can be implemented, on top of typechecking and execution of the underlying language. Moreover, programmers can handle errors due to composition operators.

Besides soundness, our technique ensures an additional important property called meta-levelsoundness, that is, typing errors never originate from (meta-)code in already compiled programs.

The paper is available at http://www.disi.unige.it/person/ServettoM/papers/ServettoZuccaSubmitted10.pdf.

Extending lambda-calculus with unbind and rebind

with M. Dezani, P. Giannini

Technical report. January 2010. Submitted for journal publication.

We extend the simply typed lambda-calculus with unbind and rebind primitive constructs. That is, a value can be a fragment of open code, which in order to be used should be explicitly rebound. This mechanism nicely coexists with standard static binding. The motivation is to provide an unifying foundation for mechanisms of dynamic scoping, where the meaning of a name is determined at runtime, rebinding, such as dynamic updating of resources and exchange of mobile code, and delegation, where an alternative action is taken if a binding is missing. Depending on the application scenario, we consider two extensions which differ in the way type safety is guaranteed. The former relies on a combination of static and dynamic type checking. That is, rebind raises a dynamic error if for some variable there is no replacing term or it has the wrong type. In the latter, this error is prevented by a purely static type system, at the price of more sophisticated types.

The paper is available at http://www.disi.unige.it/person/ZuccaE/Research/papers/ITA10.pdf.

A lightweight approach to customizable composition operators for Java-like classes

with G. Lagorio, M. Servetto

FACS'09 (Formal Aspects of Component Software), Electronic Notes in Theoretical Computer Science. To appear.

We propose a formal framework for extending a class-based language, equipped with a given class composition mechanism, to allow programmers to define their own derived composition operators. These definitions can exploit the full expressive power of the underlying computational language. The extension is obtained by adding meta-expressions, that is, expressions denoting class expressions, to conventional expressions. Such meta-expressions can appear as class definitions in the class table. Extended class tables are reduced to conventional ones by a process that we call compile-time execution, which evaluates these meta-expressions. This mechanism poses the non-trivial problem of guaranteeing soundness, that is, ensuring that the conventional class table, obtained by compile-time execution, is well-typed in the conventional sense. This problem can be tackled in many ways. In this paper, we illustrate a lightweight solution which enriches compile-time execution by partial typechecking steps. Conventional typechecking of class expressions only takes place when they appear as class definitions in the class table. With this approach, it suffices to introduce a unique common type code for meta-expressions, at the price of a later error detection.

The paper is available at http://www.disi.unige.it/person/LagorioG/papers/LAtCCO.pdf.

Customizable composition operators for Java-like classes (extended abstract)

with G. Lagorio, M. Servetto

ICTCS'09 - Italian Conference on Theoretical Computer Science

We propose a formal framework for extending a class-based language, equipped with a given class composition mechanism, to allow programmers to define their own derived composition operators. These definitions can exploit the full expressive power of the underlying computational language. The extension is obtained by adding meta-expressions, that is, (expressions denoting) class expressions, to conventional expressions. Such meta-expressions can appear as class definitions in the class table. Extended class tables are reduced to conventional ones by a process that we call compile-time execution, which evaluates these meta-expressions. This mechanism poses the non-trivial problem of guaranteeing soundness, that is, ensuring that the conventional class table, obtained by compile-time execution, is well-typed in the conventional sense. This problem can be tackled in many ways. In this paper, we illustrate a lightweight solution which enriches compile-time execution by partial typechecking steps.

The paper is available at http://www.disi.unige.it/person/LagorioG/papers/CustomOpICTCS2009.pdf.

The essence of static and dynamic bindings

with M. Dezani, P. Giannini

ICTCS'09 - Italian Conference on Theoretical Computer Science

Static binding is the standard binding discipline in programming languages. However, the demands of developing distributed, highly dynamic applications have led to an increasing interest in dynamic programming languages and mechanisms. Typically, this needs are satisfied by hoc mechanisms that lack clean semantics. In this paper, we adopt a foundational approach, developing a core dynamic rebinding mechanism as an extension of the simply typed call-by-value lambda-calculus.

The paper is available at http://www.disi.unige.it/person/ZuccaE/Research/papers/ICTCS09-DGZ.pdf.

Featherweight Jigsaw - A minimal core calculus for modular composition of classes

with G. Lagorio, M. Servetto

Sophia Drossopolou, editor, ECOOP'09 - European Conference on Object-Oriented Programming, Lecture Notes in Computer Science 5653, Springer, 2009.

We present FJig, a simple calculus where basic building blocks are classes in the style of Featherweight Java, declaring fields, methods and one constructor. However, inheritance has been generalized to the much more flexible notion originally proposed in Bracha's Jigsaw framework. That is, classes play also the role of modules, that can be composed by a rich set of operators, all of which can be expressed by a minimal core. Fields and methods can be declared of four different kinds (abstract, virtual, frozen, local) determining how they are affected by the operators. We keep the nominal approach of Java-like languages, that is, types are class names. However, a class is not necessarily a structural subtype of any class used in its defining expression. While this allows a more flexible reuse, it may prevent the (generalized) inheritance relation to be a subtyping relation. So, the required subtyping relations among classes are declared by the programmer and checked by the type system. The calculus allows the encoding of a large variety of different mechanisms for software composition in class-based languages, including standard inheritance, mixin classes, traits and hiding. Hence, FJig can be used as a unifying framework for analyzing existing mechanisms and proposing new extensions.

The paper is available at http://www.disi.unige.it/person/LagorioG/papers/FJig_core.pdf. See also the extended version with proofs.

Flattening versus direct semantics for Featherweight Jigsaw

with G. Lagorio, M. Servetto

Inheritance in object-oriented languages allows, roughly, to obtain the same effect one would get by duplicating the methods of the parent class in the heir. However, the key advantage is that source code duplication is avoided, and the code of the parent is, instead, found on demand, through a runtime procedure called method look-up. In other words, two different semantics of inheritance can be given: flattening semantics, that is, by translation into a language with no inheritance, and direct semantics, that is, by formalizing dynamic method look-up. Analogously, many other composition mechanisms, which have been proposed for enhancing the object-oriented paradigm, such as mixins and traits, can be formally defined either by translation into standard inheritance, or by a providing a direct execution model. Flattening semantics generally provides a simpler model and can be used as a guide in language design. However, it is not adequate for compositional analysis since the binary code for each code fragment, say, a class, can be generated only when all (directly or indirectly) used fragments are available. In this paper, we define both semantics and prove their equivalence for Featherweight Jigsaw, a class-based language providing a very general framework for software composition, subsuming, besides other mechanisms, standard inheritance, mixins, and traits. Then, we prove equivalence with flattening semantics.

The paper is available at http://www.disi.unige.it/person/LagorioG/papers/FJig_FlattVsDirect.pdf.

Type inference by coinductive logic programming

with D. Ancona, G. Lagorio

We propose a novel approach to constraint-based type inference based on coinductive logic programming. That is, constraint generation corresponds to translation into a conjunction of Horn clauses P, and constraint satisfaction is defined in terms of the maximal coinductive Herbrand model of P. We illustrate the approach by formally defining this translation for a small object-oriented language similar to Featherweight Java, where type annotations in field and method declarations can be omitted. In this way, we obtain a very precise type inference and provide new insights into the challenging problem of type inference for object-oriented programs. Since the approach is deliberately declarative, we define in fact a formal specification for a general class of algorithms, which can be a useful road maps to researchers. Moreover, despite we consider here a particular language, the methodology could be used in general for providing abstract specifications of type inference for different kinds of programming languages.

The paper is available at ftp://ftp.disi.unige.it/person/AnconaD/ALZ0908.pdf.

A Parametric Calculus for Mobile Open Code

with D. Ancona, S. Fagorzi

DCM'07 - Development in Computational Models. Electronic Notes in Computer Science 192, 2008.

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.

The paper is available at http://www.disi.unige.it/person/FagorziS/Papers/DCM07.pdf.

A Formal Framework for Compositional Compilation

with D. Ancona

G.F. Italiano, E. Moggi, and L. Laura, editors, Theoretical Computer Science (ICTCS'07). World Scientific.

We define a general framework for compositional compilation, meant as the ability of building an executable application by separate compilation and linking of single fragments, opposed to global compilation of the complete source application code. More precisely, compilation of a source code fragment in isolation generates a corresponding binary fragment equipped with type information, formally modeled as a typing, allowing type safe linking of fragments without re-inspecting code. We formally define a notion of soundness and completeness of compositional compilation w.r.t. global compilation, and show how linking can be in practice expressed by an entailment relation on typings. Then, we provide a sufficient condition on such entailment to ensure soundness and completeness of compositional compilation, and compare this condition with the principal typings property. Furthermore, we show that this entailment relation can often be modularly expressed by an entailment relation on type environments and a subtyping relation.

The paper is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/AZ-ICTCS07.pdf. See also the long version with proofs and examples of framework instantiation.

Type Inference for Polymorphic Methods in Java-like Languages

with D. Ancona, G. Lagorio

G.F. Italiano, E. Moggi, and L. Laura, editors, Theoretical Computer Science (ICTCS'07). World Scientific.

In languages like C++, Java and C#, typechecking algorithms require methods to be annotated with their parameter and result types, which are either fixed or constrained by a bound. We show that, surprisingly enough, it is possible to infer the polymorphic type of a method where parameter and result types are left unspecified, as happens in most functional languages. These types intuitively capture the (less restrictive) requirements on arguments needed to safely apply the method. We formalize our ideas on a minimal Java subset, for which we define a type system with polymorphic types and prove its soundness. We then describe an algorithm for type inference and prove its soundness and completeness. A prototype implementing inference of polymorphic types is available.

The paper is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/ALZ-ICTCS07.pdf. See also the long version with proofs.

A Provenly Correct Translation of Fickle into Java

with D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini

ACM Transactions on Programming Languages and Systems, 29 (2), 2007.

We present a translation from Fickle, a small object-oriented language allowing objects to change their class at run-time, into Java. The translation is provenly correct, in the sense that it preserves the static and dynamic semantics. Moreover, it is compatible with separate compilation, since the translation of a Fickle class does not depend on the implementation of used classes. Based on the formal system, we have developed an implementation. The translation turned out to be a more subtle problem than we expected. In this paper, we discuss four different possible approaches we considered for the design of the translation and justify our choice, we present formally the translation and the proof of preservation of the static and dynamic semantics, and we discuss the prototype implementation. Moreover, we outline an alternative translation based on generics that avoids most of the casts (but not all) needed in the previous translation. The language Fickle has undergone, and is still undergoing several phases of development. In this paper we are discussing the translation of FickleII.

The paper is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/PCTFJ.pdf.

A Calculus of Components with Dynamic Type-Checking

with S. Fagorzi

FACS'06 (Formal Aspects of Component Software), Electronic Notes in Theoretical Computer Science 182, 2007.

We present a simple module calculus modeling software composition in an open environment, where some components can be provided from the outside after execution has started. Operators for combining software components are as in previous module calculi; here, we focus on the new problems posed by the fact that components are not all available at compile time. In particular, we want to be able to statically check internal consistency of local code, by only specifying a required type for missing components, and then to perform dynamic checks which ensure that code received from the outside, which is assumed to travel with its type, can be successfully accepted, without requiring to type-check the whole code again.

We consider two alternative solutions. The former uses simple dynamic checks based on standard subtyping, that is, a component can be safely combined with local code if it provides the expected features, and all additional features are hidden, thus avoiding conflict problems. The latter preserves the semantics we would get having all components statically available, but requires a more involved type system based on constraints, where dynamic checks prevent conflicts.

The paper is available at http://www.disi.unige.it/person/FagorziS/Papers/FZ06.pdf.

Just: safe unknown types in Java-like languages

with G. Lagorio

Journal of Object Technology, 6(2), 2007.

Most mainstream object-oriented languages, like C++, Java and C#, are statically typed. In recent years, untyped languages, in particular scripting languages for the web, have gained a lot of popularity notwithstanding the fact that the advantages of static typing, such as earlier detection of errors, are widely accepted. We think that one of the main reasons for their widespread adoption is that, in many situations, the ability of ignoring types can be handy to write simpler and more readable code.

We propose an extension of Java-like languages which allows developers to forget about typing in strategic places of their programs without losing type-safety. That is, we allow programmers to write simpler code without sacrificing the advantages of static typing. This is achieved by means of inferred type constraints. These constraints describe the implicit requirements on untyped code to be correctly invoked.

This flexibility comes at a cost: field accesses and method invocations on objects of unknown types are less efficient than regular field accesses and method invocations. Also, our type system is currently more restrictive than it should be; its extension is the subject of ongoing work.

We have implemented our approach on a small, yet significant, Java subset.

The paper is available at http://www.jot.fm//issues/issue_2007_02/article4.pdf.

A Calculus of Open Modules: Call-by-need Strategy and Confluence

with S. Fagorzi

Mathematical Structures in Computer Science 17, 2007. Extended version of A Calculus for Reconfiguration (extended abstract).

We present a simple module calculus where selection and execution of a component is possible on open modules, that is, modules which still have to import some definitions from the outside. Hence, it provides a kernel model for a computational paradigm in which standard execution (that is, execution of a single computation described by a fragment of code) can be interleaved with operations at the meta-level which can manipulate in various ways the context in which this computation takes place. Formally, this is achieved by introducing as basic terms configurations, which are, roughly speaking, pairs consisting of an (open, mutually recursive) collection of named components and a term representing a program running in the context of these components. Configurations can be manipulated by classical module/fragment operators, hence reduction steps can be either execution steps of the program or steps which perform module operators (called reconfiguration steps). Since configurations combine the features of lambda-abstractions (first-class functions), records, environments with mutually recursive definitions, and modules, the calculus extends and integrates both traditional module calculi and recursive lambda-calculi. We state confluence of the calculus, and propose different ways to prevent errors due to lack of some needed component, either by a purely static type system or by a combination of static and run-time checks. Moreover, we define a call-by-need strategy which performs module simplification only when needed and only once, leading to a generalization, including module features, of call-by-need lambda-calculi. We prove soundness and completeness of this strategy using an approach based on information content which also allows to preserve confluence even in case local substitution rules are added to the calculus.

The paper is available at http://www.disi.unige.it/person/FagorziS/Papers/FZ06b.pdf.

Flexible Type-Safe Linking of Components for Java-like Languages

with D. Ancona and G. Lagorio

JMLC'06 (Joint Modular Languages Conference), Lecture Notes in Computer Science 4228, Springer.

We define a framework of components based on Java-like languages, where components are binary mixin modules. Basic components can be obtained from a collection of classes by compiling such classes in isolation; for allowing that, requirements in the form of type constraints are associated with each class. Requirements are specified by the user who, however, is assisted by the compiler which can generate missing constraints essential to guarantee type safety. Basic components can be composed together by using a set of expressive typed operators; thanks to soundness results, such a composition is always type safe. The framework is designed as a separate layer which can be instantiated on top of any Java-like language; to show the effectiveness of the approach, an instantiation on a small Java subset is provided, together with a prototype implementation. Besides safety, the approach achieves great flexibility in reusing components for two reasons: (1) type constraints generated for a single component exactly capture all possible contexts where it can be safely used; (2) composition of components is not limited to conventional linking, but is achieved by means of a set of powerful operators typical of mixin modules.

The paper is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/JMLC06.pdf.

Introducing Safe Unknown Types in Java-like Languages

with G. Lagorio

SAC 2006 - ACM Symposium on Applied Computing, OOPS track ACM Press.

Most mainstream object-oriented languages, like C++, Java and C#, are statically typed. In recent years, untyped languages, in particular scripting languages for the web, have gained a lot of popularity notwithstanding the fact that the advantages of static typing, such as earlier detection of errors, are widely accepted. We think that one of the main reasons for their widespread adoption is that, in many situations, the ability of ignoring types can be handy to write simpler and more readable code.

We propose an extension of Java-like languages which allows developers to forget about typing in strategic places of their programs without losing type-safety. That is, we allow programmers to write simpler code without sacrificing the advantages of static typing. This is achieved by means of inferred type constraints. These constraints describe the implicit requirements on untyped code to be correctly invoked.

This flexibility comes at a cost: field accesses and method invocations on objects of unknown types are less efficient than regular field accesses and method invocations. Also, our type system is currently more restrictive than it should be; its extension is the subject of ongoing work. However, the novel approach presented here is quite interesting on its own, as it supports separate compilation and there is zero runtime overhead on code which does not take advantage of the new features.

The paper is available at http://www.disi.unige.it/person/LagorioG/papers/LagZuc-SAC2006.pdf.

A Framework for Type Safe Exchange of Mobile Code

with S. Fagorzi

TGC 2006 - Symposium on Trustworthy Global Computing. Lecture Notes in Computer Science 4661, Springer.

We present a simple parametric calculus of processes which exchange mobile code, where type safety is ensured by a combination of static and dynamic checks. That is, internal consistency of each process is locally verified before starting execution, by only relying on type assumptions on missing code; then, at execution time, when locally typechecked code is sent from a process to another, a run-time check based on a subtyping relation ensures that it can be successfully received, without requiring to inspect code again.

The calculus is defined in a parametric way, that is, we do not fix 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 first on a simple lambda-calculus with records, and then on a calculus of mixin modules which generalizes the previous one.

The paper is available at http://www.disi.unige.it/person/FagorziS/Papers/TGC06.pdf.

A Calculus for Reconfiguration (extended abstract)

with S. Fagorzi

M. Fernández and I. Mackie editors, DCM'05 (International Workshop on Developments in Computational Models), Electronic Notes in Theoretical Computer Science 135 (3), 2006.

We present a simple calculus, called R-calculus (for "reconfiguration"), intended to provide a kernel model for a computational paradigm in which standard execution (that is, execution of a single computation described by a fragment of code) can be interleaved with operations at the meta-level which can manipulate in various ways the context in which this computation takes place. Formally, this is achieved by introducing as basic terms of the calculus "configurations", which are, roughly speaking, pairs consisting of an (open, mutually recursive) collection of named components and a term representing a "program" running in the context of these components. The R-calculus has been originally developed as a formal model for programming-in-the large, where computations correspond to applications running in some context of software components, and operations at the meta-level correspond to the possibility of dynamically loading, updating or in general manipulating these software components without stopping the application. However, the calculus can also be seen as useful for programming-in-the-small issues, because configurations combine the features of lambda-abstractions (first-class functions), records, environments with mutually recursive definitions, and modules.

We state confluence of the calculus and define a call-by-need strategy which leads to a generalization, including reconfiguration features, of call-by-need lambda-calculi.

Smart Modules for Java-like Languages

with D. Ancona and G. Lagorio

FTfJP 2005 (Formal Techniques for Java-like Programs)

We present SmartJavaMod, a language of mixin modules supporting compositional compilation, and constructed on top of the Java language. More in detail, this means that basic modules are collections of Java classes which can be typechecked in isolation, inferring constraints on missing classes and allowing safe reuse of the module in as many contexts as possible. Furthermore, it is possible to write structured module expressions by means of a set of module operators, and a type system at the module level ensures type safety, in the sense that we can always reduce a module expression to a well-formed collection of Java classes. What we obtain is a module language which is extremely flexible and allows the encoding (without any need of enriching the core level, that is, the Java language) of a variety of constructs supporting software reuse and extensibility.

The report is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/SMJL.pdf.

Compositional Compilation for Java-like Languages through Polymorphic Bytecode

with D. Ancona, F. Damiani, and S. Drossopoulou

Technical report. January 2005. Extended version of Polymorphic Bytecode: Compositional Compilation for Java-like Languages

We define compositional compilation as the ability to typecheck source code fragments in isolation, generate corresponding binaries, and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but also depends on the compilation context.

We propose a way to obtain compositional compilation for Java, by introducing a polymorphic form of bytecode containing type variables (ranging over class names) and equipped with a set of constraints involving type variables. Thus, polymorphic bytecode provides a representation for all the (standard) bytecode that can be obtained by replacing type variables with classes satisfying the associated constraints.

We illustrate our proposal by developing a typing and a linking algorithm. The typing algorithm compiles a class in isolation generating the corresponding polymorphic bytecode fragment and constraints on the classes it depends on. The linking algorithm takes a collection of polymorphic bytecode fragments, checks their mutual consistency, and possibly simplifies and specializes them. In particular, linking a self-contained collection of fragments either fails, or produces standard bytecode (the same as what would have been produced by standard compilation of all fragments).

The report is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/PBCCJL.pdf

Polymorphic Bytecode: Compositional Compilation for Java-like Languages

with D. Ancona, F. Damiani, and S. Drossopoulou

POPL'05 - ACM Symp. on Principles of Programming Languages, ACM Press.

We define compositional compilation to be the ability to typecheck source code fragments in isolation, generate corresponding binaries, and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but depends on the compilation context.

In this paper, we propose a way to obtain compositional compilation for Java, by introducing a polymorphic form of bytecode containing type variables (ranging over class names) and equipped with a set of constraints involving type variables. Thus, polymorphic bytecode provides a representation for all the (standard Java) bytecode that can be obtained by replacing type variables with class names satisfying the associated constraints.

We illustrate our proposal by developing a type inference and a linking algorithm for a small subset of Java. The type inference algorithm compiles a class in isolation generating the corresponding polymorphic bytecode fragment with the needed constraints on the classes it depends on. The linking algorithm takes a collection of polymorphic bytecode fragments, checks their mutual consistency, and possibly simplifies and specializes them. In particular, when a self-contained collection of fragments is taken, linking either fails, or produces standard Java bytecode (which is the same as the one which would have been produced by standard Java compilation of all fragments together).

The conference paper (COPYRIGHT by ACM) is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/POPL05.pdf

Mixin Modules for Dynamic Rebinding

with D. Ancona and S. Fagorzi

R. De Nicola and D. Sangiorgi, editors, TGC 2005 - Symposium on Trustworthy Global Computing. Lecture Notes in Computer Science 3705, Springer.

Dynamic rebinding is the ability of changing the definitions of names at execution time. While dynamic rebinding is clearly useful in practice, and increasingly needed in modern systems, most programming languages provide only limited and ad-hoc mechanisms, and no adequate semantic understanding currently exists.

Here, we provide a simple and powerful mechanism for dynamic rebinding by means of a calculus CMS^l,v of mixin modules (mutually recursive modules allowing redefinition of components) where, differently from the traditional approach, module operations can be performed after selecting and executing a module component: in this way, execution can refer to virtual components, which can be rebound when module operators are executed. In particular, in our calculus module operations are performed on demand, when execution would otherwise get stuck.

We provide a sound type system, which ensures that execution never tries to access module components which cannot become available, and show how the calculus can be used to encode a variety of real-world dynamic rebinding mechanisms.

The paper is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/TGC05.pdf.
See also the extended version with proofs.

A Case-Study in Encoding Configuration Languages: Multiple Class Loaders

with S. Fagorzi

Journal of Object Technology, 3 (11), Chair of Software Engineering (ETH Zurich), 2004.

The contribution of the paper is twofold. First, we define a toy language, called SJavaL, which provides a very abstract view of the mechanism of dynamic class loading with multiple loaders as in Java. The aim is to study this feature in isolation, allowing a better understanding; moreover, this also shows a stratified approach, which, differently from the Java approach based on reflection, distinguishes between the language at the user level and the configuration language. This approach is less flexible but allows to statically check type safety, hence provides an intermediate solution between the rigid approach based only on the class path and that which allows loaders to depend on execution of user applications, which can be intricate and error-prone.

The second contribution is related to a recent stream of work aiming at defining simple and powerful calculi providing a common foundation for systems supporting dynamic reconfiguration. We use SJavaL as an extended case-study, by defining an encoding in one of these kernel calculi, and prove the correctness of the translation.

The paper is available at http://www.jot.fm/issues/issue_2004_12/article2

A Calculus for Dynamic Reconfiguration with Low Priority Linking

with D. Ancona and S. Fagorzi

V. Bono, M. Bugliesi and S. Drossopoulou, editors, WOOD 2004 (Workshop on Object-Oriented Developments), Electronic Notes in Theoretical Computer Science Vol. 138 (2), 2005.

Building on our previous work, we present a simple module calculus where steps of execution of a module component can be interleaved with reconfiguration steps, that is, reductions at the module level, and execution can partly control precedence between these reconfiguration steps. This is achieved by means of a low priority link operator which is only performed when a certain component, which has not been linked yet, is both available and really needed for execution to proceed, otherwise precedence is given to the outer operators. We illustrate the expressive power of this mechanism by a number of examples.

We ensure soundness by a type system which prevents all errors in case configuration steps are performed in the initially designed order, plus a dynamic check which can throw a linkage error if some expected component is no longer available.

The paper is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/WOOD04.pdf.

A Calculus with Lazy Module Operators

with D. Ancona and S. Fagorzi

TCS 2004 (IFIP Int. Conf. on Theoretical Computer Science), Kluwer.

Modern programming environments such as those of Java and C# support dynamic loading of software fragments. More in general, we can expect that in the future systems will support more and more forms of interleaving of reconfiguration steps and standard execution steps, where the software fragments composing a program are dynamically changed and/or combined on demand and in different ways. However, existing kernel calculi providing formal foundations for module systems are based on a static view of module manipulation, in the sense that open code fragments can be flexibly combined together, but all module operators must be performed once for all before starting execution of a program, that is, evaluation of a module component. The definition of clean and powerful module calculi supporting lazy module operators, that is, operators which can be performed after the selection of some module component, is still an open problem. Here, we provide an example in this direction (the first at our knowledge), defining DCMS, an extension of the Calculus of Module Systems where module operators can be performed at execution time and, in particular, are executed on demand, that is, only when needed by the executing program. In other words, execution steps, if possible, take the precedence over reconfiguration steps. The type system of the calculus, which is proved to be sound, relies on a dependency analysis which ensures that execution will never try to access module components which cannot become available by performing reconfiguration steps.

The paper is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/TCS04.pdf

Even More Principal Typings for Java-like Languages

with D. Ancona, F. Damiani, and S. Drossopoulou

FTfJP 2004 (Formal Techniques for Java-like Programs), June 2004.

We propose an innovative type system for Java-like languages which can infer the minimal set of assumptions guaranteeing type correctness of a class c, and generate (abstract) bytecode for c, by inspecting the source code of c in isolation.

We prove the above properties of our type system by showing that it has principal typings. As well known, principal typings support compositional analysis, whereby a collection of classes can be safely linked together without further inspection of the classes' code, provided that each class has been typechecked in isolation (intra-checking), and that the mutual class assumptions are satisfied (inter-checking). We also develop an algorithm for inter-checking, and prove it correct.

The report is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/FTfJP04.pdf

Modeling Multiple Class Loaders by a Calculus for Dynamic Linking

with D. Ancona and S. Fagorzi

SAC 2004 - ACM Symposium on Applied Computing, OOPS track, ACM Press.

A recent paper proposes a calculus for modeling dynamic linking independently of the details of a particular programming environment.

Here we use a particular instantiation of this calculus to encode a toy language, called MCL, which provides an abstract view of the mechanism of dynamic class loading with multiple loaders as in Java.

The aim is twofold. On one hand, we show the effectiveness of the calculus in modeling existing loading and linking policies. On the other hand, we provide a simple formal model which allows a better understanding of Java-like loading mechanisms and also shows an intermediate solution between the rigid approach based only on the classpath and that which allows arbitrary user-defined loaders, which can be intricate and error-prone.

The paper is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/SAC04.ps.gz.

Principal Typings for Java-Like Languages

with D. Ancona

POPL'04 - ACM Symp. on Principles of Programming Languages, ACM Press.

The contribution of the paper is twofold. First, we provide a general notion of type system supporting separate compilation and inter-checking, and a formal definition of soundess and completeness of inter-checking w.r.t. global compilation. These properties are important in practice since they allow selective recompilation. In particular, we show that they are guaranteed when the type system has principal typings and provides sound and complete entailment relation between type environments and types.

The second contribution is more specific, and is an instantiation of the notion of type system previously defined for Featherweight Java [IgarashiEtAl99] with method overloading and field hiding. The aim is to show that it is possible to define type systems for Java-like languages, which, differently from those used by standard compilers, have principal typings, hence can be used as a basis for selective recompilation.

The paper is available at ftp://ftp.disi.unige.it/pub/person/AnconaD/POPL04.ps.gz.

A Calculus for Dynamic Linking

with D. Ancona and S. Fagorzi

ICTCS'03 - Italian Conference on Theoretical Computer Science. Lecture Notes in Computer Science 2841, Springer.

We define a calculus for modeling dynamic linking independently of the details of a particular programming environment.

The calculus keeps distinct at the language level the two notions of software configuration and execution, by introducing the two separate syntactic notions of linkset expression and command, respectively.

A reduction step can be either a simplification of a linkset expression, or the execution of a command w.r.t. a specific underlying software configuration denoted by a linkset expression; because of dynamic linking, these two kinds of reductions are interleaved.

The type system of the calculus, which is proved to be sound, relies on a quite accurate dependency analysis for ensuring type safety without losing the advantages offered by dynamic linking.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in ftp.disi.unige.it/pub/person/AnconaD/ICTCS03.ps.gz.

Jam - Designing a Java Extension with Mixins

with D. Ancona and G. Lagorio

ACM Transactions on Programming Languages and Systems, vol. 25(5), pages 641-712, ACM Press, 2003. (DISI-TR-99-15)

Extended version of Jam - A Smooth Extension of Java with Mixins.

In this paper we present Jam, an extension of the Java language supporting mixins, that is, parametric heir classes. A mixin declaration in Jam is similar to a Java heir class declaration, except that it does not extend a fixed parent class, but simply specifies the set of fields and methods a generic parent should provide. In this way, the same mixin can be instantiated on many parent classes, producing different heirs, thus avoiding code duplication and largely improving modularity and reuse. Moreover, as happens for classes and interfaces, mixin names are reference types, and all the classes obtained by instantiating the same mixin are considered subtypes of the corresponding type, hence can be handled in a uniform way through the common interface. This possibility allows a programming style where different ingredients are "mixed" together in defining a class; this paradigm is somewhat similar to that based on multiple inheritance, but avoids its complication.

The language has been designed with the main objective in mind to obtain, rather than a new theoretical language, a working and smooth extension of Java. That means, on the design side, that we have faced the challenging problem of integrating the Java overall principles and complex type system with this new notion; on the implementation side, that we have developed a Jam to Java translator which makes Jam sources executable on every Java Virtual Machine.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/TOPLAS03.ps.gz.

Mixin Modules and Computational Effects

with D. Ancona, S.Fagorzi, E.Moggi

ICALP'03 - International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 2719, Springer.

We define a calculus for investigating the interactions between mixin modules and computational effects, by combining the purely functional mixin calculus CMS with a monadic metalanguage supporting the two separate notions of simplification (local evaluation with no side-effects) and computation (global evaluation able to modify the store). This distinction is important for smoothly integrating the CMS rules (which are all local) with the rules dealing with the imperative features.

In our calculus mixins can contain mutually recursive computational components which are explicitly computed by means of a new mixin operator whose semantics is defined in terms of a Haskell-like recursive monadic binding.

Since we mainly focus on the operational aspects, we adopt a simple type system like that for Haskell, that does not detect dynamic errors related to bad recursive declarations involving effects.

The calculus serves as a formal basis for defining the semantics of imperative programming languages supporting first class mixins while preserving the CMS equational reasoning.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in . /pub/person/AnconaD/ICALP03.ps.gz

For a longer version see also /pub/person/AnconaD/longICALP03.ps.gz

A Theory of Mixin Modules: Algebraic Laws and Reduction Semantics

with D. Ancona

Mathematical Structures in Computer Science, vol. 12, pages 1-37. Cambridge University Press, 2002. (DISI-TR-99-05)

Extended version of An Algebra of Mixin Modules.

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.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/MSCS01.ps.gz.

True Separate Compilation of Java Classes

with D. Ancona and G. Lagorio

PPDP'02, International Conference of Principles and Practice of Declarative Programming, ACM Press, 2002.

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. These requirements are specified by a local type environment associated with each single class, while in the existing formal definitions of the Java type system classes are typed in a global type environment containing all the type information on a closed program. We also provide formal rules for static inter-checking and relate our approach with compilation of closed programs, by proving that we get the same results.

An extended abstract of this paper is available in compressed postscript through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/TrueSepComp.ps.gz The long version paper is available in /pub/person/AnconaD/TrueSepCompLong.ps.gz

Simplifying types in a calculus for Java exceptions

with G. Lagorio and E. Zucca

Technical report, DISI. December 2003. Submitted for journal publication.

Extended version of A Core Calculus for Java Exceptions.

In this paper we present a simple calculus (called CJE) in order to fully investigate the exception mechanism of Java (in particular its interaction with inheritance). We first define a type system for the calculus, called FULL, directly driven by the Java Language Specification and prove its soundness; then, we show that this type system uses redundant types and we formally capture this fact by defining equivalence relations on types and by proving that the static semantics of CJE programs is preserved under these equivalences; furthermore, for each type we show that there exists the smallest equivalent type. Finally, we propose a simplification of the Java specification concerning throws clause which minimally affects the expressive power of the language.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/SimplExc.ps.gz.

A Formal Framework for Java Separate Compilation

with D. Ancona and G. Lagorio

ECOOP'02 - European Conference on Object-Oriented Programming, Lecture Notes in Computer Science 2374, Springer.

We define a formal notion, called compilation schema, allowing to specify different possibilities for performing the overall process of Java compilation, which includes type-checking of source fragments with generation of corresponding binary code, type-checking of binary fragments, extraction of type information from fragments and definition of dependencies among them. We consider three compilation schemata of interest for Java, that is, minimal, SDK and safe, which correspond to a minimal set of checks, the checks performed by the SDK implementation, and all the checks needed to prevent run-time linkage errors, respectively. In order to demonstrate our approach, we define a kernel model for Java separate compilation and execution, consisting in a small Java subset, and a simple corresponding binary language for which we provide an operational semantics including run-time verification. We define a safe compilation schema for this language and formally prove type safety.

This paper is available in compressed postscript through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/ECOOP02.ps.gz

A type preserving translation of Fickle into Java

with D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini

U. Montanari editor, TOSCA 2001 - Theory of Concurrency, Higher Order and Types Workshop 2002, Electronic Notes in Theoretical Computer Science Vol. 62, 2002.

We present a translation from Fickle (a Java-like language allowing objects that can change their class at run-time) into plain Java. The translation, which maps any Fickle class into a Java class, is driven by an invariant that relates the Fickle object to its Java counterpart. The translation, which is proven to preserve both the static and the dynamic semantics of the language, is an enhanced version of a previous proposal by the same authors.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/ENTCS02.ps.gz.

A Calculus of Module Systems

with D. Ancona

Journal of Functional Programming 12(2), 2002. (DISI-TR-99-09)

Extended version of A Primitive Calculus of Module Systems.

We present CMS, a simple and powerful calculus of modules supporting mutual recursion and higher order features, which can be instantiated over an arbitrary core calculus satisfying standard assumptions.

The calculus allows expression of a large variety of existing mechanisms for combining software components, including parameterized modules similar to ML functors, extension with overriding as in object-oriented programming, mixin modules and extra-linguistic mechanisms like those provided by a linker. Hence CMS can be used as a paradigmatic calculus for modular languages, in the same spirit the lambda calculus is used for functional programming.

We first present an untyped version of the calculus and then a type system; we proveconfluence, progress, and subject reduction properties. Then, wedefine a derived calculus of mixin modules directly in terms of CMSand show howto encode other primitive calculi into CMS (the lambda calculus and the Abadi-Cardelliobject calculus). Finally, we consider the problem of introducing a subtype relation for module types.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in ftp://ftp.disi.unige.it/pub/person/AnconaD/cms_journal.ps.gz.

A Core Calculus for Java Exceptions

with D. Ancona and G. Lagorio

OOPSLA'01 - International Conference on Object-Oriented Programming, Systems and Applications, SIGPLAN Notices, ACM Press, October 2001. (DISI-TR-00-16)

Extended version of A Core Calculus for Java Exceptions (extended abstract).

In this paper we present a simple calculus (called CJE) in order to fully investigate the exception mechanism of Java (in particular its interaction with inheritance). We first define a type system for the calculus, called FULL, directly driven by the Java Language Specification; then, we show that this type system uses too many types, in the sense that there are different types which turn out to be equivalent, since they provide exactly the same type information. Hence, we obtain from FULL a simplified type system called MIN where equivalent types have been identified. We show, in particular, that both FULL and MIN are equivalent and can be obtained as instantiations of a type system parametric in a number of operations on types used in the typing rules. Such operations form a pair of algebras whose properties are useful both for type-checking optimization and for clarifying the static semantics of the language. The two type systems are proved to satisfy the subject reduction property.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/OOPSLA01.ps.gz.

An Effective Translation of Fickle into Java

with D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini

ICTCS'01 - Italian Conference on Theoretical Computer Science, Lecture Notes in Computer Science 2202, Springer.

We present a translation from Fickle (a Java-like language allowing dynamic object re-classification, that is, objects that can change their class at run-time) into plain Java. The translation is proved to preserve static and dynamic semantics; moreover, it is shown to be effective, in the sense that the translation of a Fickle class does not depend on the implementation of used classes, hence can be done in a separate way, that is, without having their sources, exactly as it happens for Java compilation. The aim is to demonstrate that an extension of Java supporting dynamic object re-classification could be fully compatible with the existing Java environment.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/Fickle.ps.gz.

Java Separate Type Checking is not Safe

with D. Ancona and G. Lagorio

FTfJP 2001 (Formal Techniques for Java Programs), June 2001.

Java supports separate type-checking in the sense that compilation can be invoked on a single source fragment, and this may enforce type-checking of other either source or binary fragments existing in the environment. However, the Java specification does not define precise rules on how this process should be performed, therefore the outcome of compilation may strongly depend on the particular compiler implementation. Furthermore, rules adopted by standard Java compilers, as SDK and Jikes, can produce binary fragments whose execution throws linking related errors. We introduce a simple framework which allows to formally express the process of separate compilation and the related formal notion of type safety. Moreover, we define, for a small subset of Java, a type system for separate compilation which we conjecture to be safe.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/ECOOPWS01.ps.gz.

True Modules for Java-Like Languages

with D. Ancona

ECOOP'01 - European Conference on Object-Oriented Programming, Lecture Notes in Computer Science 2072, Springer. (DISI-TR-00-12)

We present JavaMod, a true module system constructed on top of the Java language. More in detail, this means that basic modules are collections of Java classes and specify in their interface the imported and exported classes with their types; furthermore, it is possible to write structured module expressions by means of a set of module operators and a type system at the module level ensures type safety.

In designing such a type system, one has to face non trivial problems, notably the fact that a module M which extends an imported class C can be correctly combined only with modules exporting a class C which, besides providing the expected services, causes no interferences with its subclasses defined in M.

What we obtain is a module language which is extremely flexible and allows to express (without any need of enriching the core level, that is, the Java language), for instance, generic types as in Pizza and GJ, mixin classes (that is, heir classes parametric in the superclass) and mutually recursive class definitions split in independent modules.

We provide a semantics for JavaMod by translation in a module calculus MiniJavaMod which is very close to the high-level language, but has more primitive operators on modules and is defined on top of a core language where is possible to annotate parent classes with the required type.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/JavaMod.ps.gz.

An extended version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/DISI-TR-00-12.ps.gz

Overloading and Inheritance

with D. Ancona and S. Drossopoulou

FOOL 8, London, January 2001.

Overloading allows several function definitions for the same name, distinguished primarily through different argument types; it is typically resolved at compile-time. Inheritance allows subclasses to define more special versions of the same function; it is typically resolved at run-time.

Modern object-oriented languages incorporate both features, usually in a type-safe manner. However, the combination of these features sometimes turns out to have surprising, and even counterintuitive, effects.

We discuss why we consider these effects inappropriate, and suggest alternatives. We explore the design space by isolating the main issues involved and analyzing their interplay and suggest a formal framework describing static overloading resolution and dynamic function selection, in a programming language, and their abstracting from other language features. We believe that our framework clarifies the thought process going on at language design level.

We introduce a notion of soundness and completeness of an overloading resolution policy w.r.t. the underlying dynamic semantics, and a way of comparing the flexibility of different resolution policies. We apply these concepts to some non-trivial issues raised in concrete languages.

We also argue that the semantics of overloading and inheritance is "clean" only if it can be understood through a copy semantics, whereby programs are transformed to equivalent programs without subclasses, and the effect of inheritance is obtained through copying.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/FOOL8.ps.gz.

A Core Calculus for Java Exceptions

with D. Ancona and G. Lagorio

FTfJP 2000- (Formal Techniques for Java Programs), June 2000.

An extended version of this paper is A Core Calculus for Java Exceptions

In this paper we present a simple calculus (called CJE) corresponding to a small functional fragment of Java supporting exceptions. We provide a reduction semantics for the calculus together with two different but equivalent type systems; the first corresponds to the Java Language Specification and its formalization provided by Drossopolou, Valkevych and Eisenbach, whereas the second can be considered as a sort of optimization of the first where only the minimal type information about classes/interfaces and methods are collected in order to successfully type-check a program. The two systems are proved to be equivalent and a subject reduction theorem is given.

The compressed postscript version of this paper is available through anonymous ftp in /pub/person/AnconaD/ECOOPWSExceptions.ps.gz.

Overloading and Inheritance in Java

with D. Ancona and S. Drossopoulou

FTfJP 2000 (Formal Techniques for Java Programs), June 2000.

The combination of overloading and inheritance in Java introduces questions about function selection, and makes some function calls ambiguous. We believe that the approach taken by Java designers is counterintuitive.

We explore an alternative, and argue that it is more intuitive and agrees with the Java rules for the cases where Java considers the function calls unambiguous, but gives meaning to more calls than Java does.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/JavaOverloading.ps.gz.

Extending Casl with Late Binding

with D. Ancona and M. Cerioli

Recent Trends in Algebraic Development Techniques (14th Workshop, WADT '99 - Selected Papers), Lecture Notes in Computer Science 1827, Springer, 2000. (DISI-TR-99-14)

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 LBInst 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.

In addition to this, we propose a further enrichment of the Casl language which is made possible by introduction of late binding, that is a mechanism for "inheriting" axioms from a supersort with the possibility of overriding them. The aim is to obtain advantages in terms of reuse of specifications similar to those obtained by inheritance in object-oriented programming languages.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/DISI-TR-99-14.ps.gz.

Jam: A Smooth Extension of Java with Mixins

with D. Ancona and G. Lagorio

E. Bertino, editor, ECOOP'00 - European Conference on Object-Oriented Programming, Lecture Notes in Computer Science 1850, Springer.

An extended version of this paper is Jam - Theory and Practice of a Java Extension with Mixins

In this paper we present Jam, an extension of the Java language supporting mixins, also called parametric heir classes. A mixin declaration in Jam is similar to a Java heir class declaration, apart that it does not extend a fixed parent class, but simply specifies the set of fields and methods a generic parent should provide. In this way, the same mixin can be instantiated on many parent classes, producing different heirs, thus avoiding code duplication and largely improving modularity and reuse. Moreover, as happens for classes and interfaces, mixin names are reference types, and all the classes obtained instantiating the same mixin are considered subtypes of the corresponding type, hence can be handled in a uniform way through the common interface. This possibility allows a programming style where different ingredients are "mixed" together in defining a class; this paradigm is partly similar to that based on multiple inheritance, but avoids its complication.

The language has been designed with the main objective in mind to obtain, rather than a new theoretical language, a working and smooth extension of Java. That means, on the design side, that we have faced the challenging problem of integrating the Java overall principles and complex type system with this new notion; on the implementation side, that we have developed a Jam to Java translator which makes Jam sources executable on every Java Virtual Machine.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/ECOOP00.ps.gz.

Deriving Proof Rules from Continuation Semantics

with P. Audebaud

Formal Aspects of Computing 11(4), pages 426-447, 1999. (RR 97-19, LIP-ENS Lyon, 1997)

We claim that the continuation style semantics of a programming language can provide a starting point for constructing a proof system for that language. The basic idea is to see weakest precondition as a particular instance of continuation style semantics, hence to interpret correctness assertions (e.g. Hoare triples) as inequalities over continuations. This approach also shows a correspondence between labels in a program and annotations.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/FAC99.ps.gz.

A Primitive Calculus for Module Systems

with D. Ancona

G. Nadathur editor, PPDP'99 - International Conference of Principles and Practice of Declarative Programming, Lecture Notes in Computer Science 1702, Springer.

An extended version of this paper is A Calculus of Module Systems

We present a simple and powerful calculus of modules supporting mutual recursion and higher order features.

The calculus allows to encode a large variety of existing mechanisms for combining software components, including parameterized modules like ML functors, extension with overriding of object-oriented programming, mixin modules and extra-linguistic mechanisms like those provided by a linker.

As usual, we first present an untyped version of our calculus and then a type system which is proved sound w.r.t. the reduction semantics; moreover we give a translation of other primitive calculi.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/cms.ps.gz.

An interpreter for the calculus can be found at www.disi.unige.it/person/AnconaD/Java/UPCMS.html

A Formal Framework with Late Binding

with D. Ancona and M. Cerioli

FASE'99 - Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science 1577, Springer. (DISI-TR-98-16, 1998)

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.

The compressed postscript version of this paper is available through anonymous ftp at /pub/person/Ancona/FASE99.ps.gz. The technical report version, including proofs, is available through anonymous ftp at /pub/person/Ancona/DISI-TR-98-16.ps.gz.

An extended abstract (postcript version), included in the proceedings of the first workshop of the project "Tecniche formali per la specifica, l'analisi, la verifica, la sintesi e la trasformazione di sistemi software" is available through anonymous ftp at /pub/person/ZuccaE/P40Abstract.dvi.ps.

Stores as Homomorphisms and Their Transformations - A Uniform Approach to Structured Types in Imperative Languages

Science of Computer Programming, Vol. 34 Issue 3, pages 163-190, June 1999. (DISI-TR-94-14, 1994)

Extended version of Stores as Homomorphisms and Their Transformations.

We address the problem of giving a clean and uniform mathematical model for handling user defined data types in imperative languages, contrary to the ad-hoc treatment usual in classical denotational semantics. The problem is solved by defining the store as a homomorphic mapping of an algebraic structure of left values modelling containers into another one of right values modelling contents. Consequently store transformations can be defined uniformly on the principle that they are minimal variations of the store embedding some basic intended effects and compatible with the homomorphic structure of the store.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/SCP99.ps.gz.

From Static to Dynamic Abstract Data-Types: An Institution Transformation

Theoretical Computer Science, Vol. 216, Issue 1/2, pages 109-157, March 1999. (DISI-TR-96-1)

Extended version of From Static to Dynamic Abstract Data-Types.

We show how to extend in a canonical way a given formalism for specifying (static) data types (like usual algebraic specification frameworks) with dynamic features. What we obtain in this way is a corresponding formalism for specifying dynamic data-types based on the "state-as-algebra" approach: a dynamic data-type models a dynamically evolving system in which any state can be viewed as a static data type in the underlying formalism, and the dynamic evolution is given by operations handling configurations. Formally, our construction is a functor between two appropriate categories of (specialized) institutions.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/TCS99.ps.gz.

A Theory of Modules with State

with D. Ancona

Technical Report, DISI-TR-98-10, 1998.

Extended version of A Formal Framework for Modules with State.

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.
Thank 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.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/Ancona/DISI-TR-98-10.ps.gz.

A Theory of Mixin Modules: Basic and Derived Operators

with D. Ancona

Mathematical Structures in Computer Science, Vol.8, number 4, pages 401-446, August 1998. (DISI-TR-96-24)

Extended version of An Algebraic Approach to Mixins and Modularity.

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.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/DISI-TR-96-24.ps.gz.

An Algebra of Mixin Modules

with D. Ancona

F. Parisi Presicce, editor, Recent Trends in Algebraic Development Techniques (12th Workshop, WADT '97 - Selected Papers), Lecture Notes in Computer Science 1376, Springer, 1998.

An extended version of this paper is A Theory of Mixin Modules: Algebraic Laws and Reduction Semantics.

In this paper we give the definition of an algebra of mixin modules. A mixin is a module which contains deferred components, i.e. components to be imported from another module; a binary and commutative operator of merge allows to associate deferred components of one mixin with the corresponding definitions (if any) of the other, allowing recursive definitions to span module boundaries. We give an axiomatic definition of a set of operations for mixin combination, including, among others, merge, overriding and functional composition. We show that such operators can be expressed by three primitive operations (namely, sum, reduct and freeze), by proving that axioms for high-level operations can be derived by the axioms of the algebra of primitive operations. Finally, we define an algebraic model of mixin satisfying the axioms of the algebra; a categorical approach allows the model to be independent of the (semantics of the) core language used for building mixin definitions.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/WADT97.ps.gz.

Implementation of Derived Programs (Almost) for Free - An Institutional Approach

with M. Cerioli

F. Parisi Presicce, editor, Recent Trends in Algebraic Development Techniques (12th Workshop, WADT '97 - Selected Papers), Lecture Notes in Computer Science 1376, Springer, 1998.

In the process of top-down software development, an implementation step can consists of two different kinds of refinement: - within the same formalism (replacing a module A by a more specific module B which simulates the behaviour of A); - between different formalisms (passing from a more to a less abstract specification or programming language).
A property that we usually expect to hold is that these two kinds of refinement can be composed, i.e, if a module A is correctly implemented by B, then all the programs which use A can be correctly transformed in programs which use B, provided that we are able to translate linguistic constructs from the more to the less abstract level.
Our aim is to give a model for this situation independent from the particular formalisms which are involved, in the spirit of the theory of institutions.
To this end, we introduce a notion which is partly similar to that of parchment (syntactic representation of an institution), since we assume that in a given formalism the expressions over a signature can be defined as a free standard many-sorted algebra.
Anyway, we require a much stronger uniformity w.r.t. parchments, since this free algebra is independent from the specific signature. That corresponds to the fact that in many concrete cases the expressions of the formalism can be defined once at all in an inductive way as terms, and any specific signature only gives a family of symbols which can be used as variables in the corresponding terms. In this case, it is actually possible to factorize an implementation step in a uniform and a specific part, the latter only depending on the particular program.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/CerioliM/WADT97.ps.gz.

Overriding Operators in a Mixin-Based Framework

with D. Ancona

H. Glaser, P.Hartel and H.Kuchen, editors, PLILP'97 - 9th Intl. Symp. on Programming Languages, Implementations, Logics and Programs, Lecture Notes in Computer Science, Springer.

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.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/PLILP97.ps.gz.

An Algebraic Approach to Mixins and Modularity

with D. Ancona

M. Hanus and M. Rodriguez Artalejo, editors, ALP '96 - 5th Intl. Conf. on Algebraic and Logic Programming, Lecture Notes in Computer Science 1139, Springer, 1996.

An extended version of this paper is A Theory of Mixin Modules: Basic and Derived Operators .

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.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/ALP96.ps.gz.

A Formal Framework for Modules with State

with D. Ancona

M. Wirsing and M. Nivat, editors, AMAST '96 - Algebraic Methodology and Software Technology, Lecture Notes in Computer Science 1101, Springer.

An extended version of this paper is A Theory of Modules with State.

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.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/AMAST96.ps.gz.

From Static to Dynamic Abstract Data-Types

W. Penczek and A. Szalas, editors, Mathematical Foundations of Computer Science 1996, Lecture Notes in Computer Science 1113, Springer.

An extended version of this paper is From Static to Dynamic Abstract Data-Types: An Institution Transformation

We show how to extend in a canonical way a given formalism for specifying (static) data types (like usual algebraic specification frameworks) with dynamic features. What we obtain in this way is a corresponding formalism for specifying dynamic data-types based on the "state-as-algebra" approach: a dynamic data-type models a dynamically evolving system in which any state can be viewed as a static data type in the underlying formalism, and the dynamic evolution is given by operations handling states. Formally, our construction is a transformation of (pre)institutions.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/MFCS96.ps.gz.

An Algebraic Semantic Framework for Object Oriented Languages with Concurrency (Extended Abstract, 10 pages)

Formal Aspects of Computing, Vol.8, number 6, pages 706-715, 1996.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/FAC96Short.ps.gz.

An Algebraic Semantic Framework for Object Oriented Languages with Concurrency (Full Version, 45 pages)

Formal Aspects of Computing (electronic supplement), Vol.8E, number 6, 1996. (DISI-TR-95-02)

Improved version of An Algebraic Compositional Semantics of an Object Oriented Notation with Concurrency

This paper presents an algebraic semantics for a schema of object oriented languages including concurrent features. A class, the basic syntactic unit of object oriented languages, denotes a set of algebras determined by an algebraic specification. This specification describes a system of (possibly active) objects interacting via method calls. Extending other approaches, structured classes are modelled in a fully compositional way. This means that the semantic counterpart of class combinators like inheritance and clientship are specification combinators. A model of records with sharing allows us to describe typical object oriented features like object sharing, inheritance polymorphism and dynamic binding. For modelling how objects evolve in a concurrent environment, we rely on an algebraic description of labelled transition systems.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/FAC96Full.ps.gz. The paper is also available here.

A Free Construction of Dynamic Terms

Journal of Computer and System Sciences. Vol. 52, number 1, pages 143-156, February 1996. (DISI-TR-94-25)

In this paper we show that it is possible to extend in a natural way to the dynamic case some basic results of the classical approach to (static) data types. Within an appropriate framework of dynamic structures (called d-oids), which play the same role of algebras in the static case, we define a language of dynamic terms, also enjoying the property of unique canonical representation; moreover dynamic terms constitute a free structure whenever the static terms in the underlying static framework are so. As a main application of the above construction, we get a rather elegant kernel language for recursive definitions of dynamic derived operations, which parallels the well-known McCarthy's schema for a kernel applicative language. This kernel language can be seen also as a metalanguage for expressing the semantics of concrete (e.g. imperative or object based) languages.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/JCSS.ps.gz.

Implementation of Data Structures in an Imperative Framework

Recent Trends in Data Type Specification (10th Workshop on Specification of Abstract Data Types, joint with the 5th COMPASS Workshop, Selected Papers) Lecture Notes in Computer Science 906, Springer, 1995. (DISI-TR-94-28)

We present a formal definition of implementation between concrete structures within the framework of dynamic data-types. The main outcome is an adequate and uniform semantic model for stating when a software module in an imperative or object based language is a correct implementation of a data structure. Moreover, the definition is obtained extending in a natural way the notion used in the static case, showing that our dynamic frameworks are a "sound" generalization of static frameworks.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/WADT94.ps.gz.

D-oids: a Model for Dynamic Data-Types

Mathematical Structures in Computer Science. Vol. 5 number 2, pages 257-282, June 1995. (DISI-TR-94-16)

We propose a semantic framework for dynamic systems which, in a sense, extends the well-known algebraic approach for modeling static data structures to the dynamic case.
The framework is based on a new mathematical structure, called d-oid, consisting of a set of instant structures and a set of dynamic operations. An instant structure is a static structure, e.g. an algebra; a dynamic operation is a transformation of instant structures with an associated point to point map, which allows to keep track of the transformations of single objects and thus is called tracking map. By an appropriate notion of morphism the d-oids over a dynamic signature constitute a category.
It is shown that d-oids can model object systems and support an abstract notion of possibly unique object identity; moreover, for a d-oid satisfying an identity preserving condition, there exist an essentially equivalent d-oid where the elements of instant structures are just names.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/MSCS.ps.gz.

Towards a Classification of Inheritance Relations.

U. W. Lipeck and G. Koschorreck, editors, Proc. ISCORE '93 (International Workshop on Information Systems - Correctness and Reusability) Informatik-Berichte 01/93, Universitaet Hannover, pages 90-113, September 1993.

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.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/IWIS93.ps.gz. The paper is also available here.

A Semantic Model for Dynamic Systems

U.W. Lipeck, B.Thalheim, editors, Modelling Database Dynamics (4th Workshop on Foundations of Models and Languages for Data and Objects, Selected Papers). Workshops in Computing, Springer, 1993.

We present a new formal structure, called d-oid, for modelling systems of evolving objects. In our view, d-oids are the dynamic counterpart of many-sorted algebras, in the sense that they can model dynamic structures as much as algebras can model static data types. D-oids are a basis for giving syntax and semantics for kernel languages for defining methods; these languages are built over what we call method expressions, like applicative kernel languages are built over terms. Moreover some hints are given towards modelling classes and inheritance.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/Volkse.ps.gz.

Stores as Homomorphisms and Their Transformations

A.M. Borzyszkowsky and S. Sokolowsky, editors, Mathematical Foundations of Computer Science 1993, Lecture Notes in Computer Science 711, Springer, 1993.

An extended version of this paper is Stores as Homomorphisms and Their Transformations - A Uniform Approach to Structured Types in Imperative Languages.

In the classical denotational model of imperative languages handling structured types, like arrays, requires an ad-hoc treatment for each data type, including e.g. an ad-hoc allocation and deallocation mechanism. Our aim is to give a homogeneous approach that can be followed whichever is the data structure of the language.
We start from the traditional model for Pascal-like languages, which uses a notion of store as a mapping from left values (containers for values, usually called locations), into right values; we combine this idea with the well-known algebraic approach for modelling data types. More precisely, we consider an algebraic structure both for the right and the left values; consequently, the store becomes a homomorphic mapping of the left into the right structure.
Seeing a store as a homomorphism has a number of interesting consequences. First of all, the transformations over a store can be uniformly and rigorously defined on the basis of the principle that they are minimal variations compatible with some basic intended effect (e.g., some elementary substitution). Thus semantic clauses too, which rely on these transformations as auxiliary functions, can be given uniformly; for example, we can give a unique clause for assignment for any data type in Pascal and Ada-like languages.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/MFCS93.ps.gz.

An Algebraic Compositional Semantics of an Object Oriented Notation with Concurrency

C.E. Veni Madhavan, editor, Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science 405, Springer, 1989.

An improved version of this paper is An Algebraic Semantic Framework for Object Oriented Languages with Concurrency.

This paper presents an algebraic compositional semantics for a schema of an object-oriented syntax which models many existing features as class hierarchies, polymorphism and concurrency, using a pattern which could be applied to different concrete languages. The semantics is defined in a classical denotational style, i.e. giving an abstract syntax, the semantic domains and the interpretation of the syntactic operators.
The given semantics is algebraic in the sense that the value denoted by a class is a class of algebras described by an algebraic specification. A class combinator (e.g. inheritance) is semantically interpreted in this framework as a function which handles classes of algebras or, in an equivalent way, as a specification combinator. Moreover, our schema of semantic definition allows to model also concurrent features if any, by underlying an approach to concurrency based on algebraic transition systems.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/FST-TCS89.ps.gz.