Genova - Third year Progress Report

Researchers: E.Moggi, G.Rosolini, E.Zucca, D.Ancona.
PhD students: C.Calcagno, G.Lagorio, L.Paolini.

Achievements

Topic A

[ADZ00] and [ADZ01] propose a simple formal framework for modeling the overloading resolution and run-time method selection in object-oriented languages, and analyze on this basis the policy of existing languages, notably Java, pointing out problems and proposing changes. [TOPIC A]
[ALZ00] and [ALZ00a] define a simple calculus which models the exception mechanism in Java, and different type systems which illustrate how the type information needed for checking exceptions can be kept minimal. [TOPIC A]
[CO01] shows that previous program logics for pointers are unsound in the presence of garbage collection, and gives a new logic, based on a non standard interpretation of quantifiers, that captures two natural notions of equivalence between programs. [TOPIC A]

Topic B

[Anc00] defines a language of mixin modules MIX(FL) constructed on top of a simple functional language. The language is strongly typed and supports separate compilation. The denotational semantics of the language is based on an algebraic approach. [TOPIC B]
[AM00] shows how it is possible to define a rather rich language of mixin modules suitable for combining together large logic programs without changing the underlying logic. [TOPIC B]
[AZ01] shows the design and a type system for a language of true modules constructed on top of a Java-like language, solving in particular the problem of correctly typing module composition in the case of classes which extend imported classes. [TOPIC B]
[ALZ01] extends the work on Jam (a Java extension with mixin classes, that is, parametric heir classes) developed in the Second Year by defining the full type system of Jam and a formal translation into pure Java which preserves type soundness. [TOPIC B]
[ALZ01a] defines an abstract framework for modeling separate compilation and expressing desirable properties a compilation function should satisfy, like monotonicity (re-compilation of a subset of source fragments is contained in re-compilation of the whole program); moreover the compilation in Java is analyzed w.r.t. these properties. [TOPIC B]
[CM00] and [CMST01] extend [CMT00] with the identification of a larger set of closed types and the addition of a binder for useless variables. The resulting language is a conservative extension of an imperative subset of SML. [TOPIC B and E]
[MS??] gives an account of monadic encapsulation of computational effects (namely state) in a CBN functional language (based on system Fw), both in the case of a strict and a lazy state semantics. [TOPIC B]

Topic D

[CR00] characterises those exact completions which are cartesian closed and those which are locally cartesian closed purely in terms of the category generating the completion. This result has been applied in several instances in the recent literature. [TOPIC D]
[FR??] produce a complete characterisation of the full embedding of the category of w-cpo's in the model H of Synthetic Domain Theory, showing that the categorical intuition and the logical intuition match very closely. [TOPIC D]
[PR??] produce a generic argument for the computation of fixpoints for domain equations. It will be applied to parametric models of domains. [TOPIC D-I]

Topic G

[Cal01] presents a novel approach, based on stratified operational semantics, for proving safety and correctness of Tofte and Talpin's region calculus. [TOPIC G]
[CHT01] considers two semantics for Tofte and Talpin's region calculus: with and without explicit references. Type safety results are proved directly and the two semantics are related to the original semantics by Tofte and Talpin. [TOPIC G]

References

[AM00] D.Ancona, V.Masardi. Mixin-based modules for logic programming. To appear in APPIA-GULP-PRODE 2000. 2000 Joint Conference on Declarative Programming. La Habana, Cuba.
[Anc00] D.Ancona. MIX(FL): a Kernel Language of Mixin Modules. AMAST 2000 - Algebraic Methodology and Software Technology, LNCS 1816, Springer Verlag, 2000.
[ADZ00] D.Ancona, S.Drossopoulou, E.Zucca. Overloading and Inheritance in Java. ECOOP'00 Workshop on Formal Techniques for Java Programs, June 2000.
[ADZ01] D.Ancona, S.Drossopoulou, E.Zucca. Overloading and Inheritance. FOOL 8, London, January 2001.
[ALZ00] D.Ancona, G.Lagorio, E.Zucca. A Core Calculus for Java Exceptions (Extended Abstract). ECOOP'00 Workshop on Formal Techniques for Java Programs, June 2000.
[ALZ00a] D.Ancona, G.Lagorio, E.Zucca. A Core Calculus for Java Exceptions. Technical Report, DISI, DISI-TR-00-16.
[AZ01] D.Ancona, E.Zucca. True Modules for Java-Like Languages. To appear in ECOOP'01, LNCS, Springer Verlag, 2001 (DISI-TR-00-12).
[ALZ01] D.Ancona, G.Lagorio, E.Zucca. Jam - Theory and Practice of a Java Extension with Mixins. Technical Report, DISI, DISI-TR-99-15. Submitted for journal publication, January 2001.
[ALZ01a] D.Ancona, G.Lagorio, E.Zucca. Monotone Separate Compilation in Java with D. Ancona and G. Lagorio. Technical Report, DISI. Submitted for publication, March 2001.
[Cal01] C.Calcagno, Stratified Operational Semantics for Safety and Correctness of Region Calculus, POPL 01, 2001.
[CHT01] C.Calcagno, S.Helsen, P.Thiemann. Syntactic Type Soundness Results for the Region Calculus. Submitted, February 2001
[CIO00] C.Calcagno, S.Ishtiaq, P.W.O'Hearn, Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare Logic, PPDP 00, 2000.
[CM00] C.Calcagno, E.Moggi, Multi-Stage Imperative Languages: A Conservative Extension Result, SAIG, 2000.
[CMT00] C.Calcagno, E.Moggi, W.Taha, Closed Types as a Simple Approach to Safe Imperative Multi-Stage Programming, ICALP 2000, LNCS, 2000.
[CMST01] C.Calcagno, E.Moggi, T.Sheard, W.Taha. Closed Types for a Safe Imperative MetaML. Submitted, March 2001.
[CO01] C.Calcagno, P.W.O'Hearn. On Garbage and Program Logic. In FOSSACS, LNCS, 2001.
[CR00] A.Carboni, G.Rosolini. Locally cartesian closed exact completions. J.Pure Appl. Alg. 154, 2000, p. 103-116
[FR??] M.Fiore, G.Rosolini. Domains in H. To appear in Theo.Comp.Sci.
[MS??] E.Moggi, A.Sabry, Monadic Encapsulation of Effects: A Revised Approach (Extended Version), Journal of Functional Programming, to appear.
[PR??] A.J. Power and G. Rosolini. Fixpoint operators for domain equations. To appear in Theo.Comp.Sci.
[R00] G.Rosolini. Equilogical spaces and filter spaces. Rend. Circ. Mat. Palermo 64, 2000, p. 157-175

Visits

Besides the interactions funded by APPSEM the following visits were relevant to the project:

C.Calcagno visited Yale and CMU (10-27/02/2001 - Genova and CMU funding)
B.Reus visited Genova (24/09/2000 - Genova funding)
M.Fiore visited Genova (01-07/09/2000 - Genova funding)
A.Simpson visited Genova (23/07/2000 - Genova funding)
K.Fisher visited Genova (24/04/2000 - Genova funding)