Genova - Second year Progress Report

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

Achievements

[AZ99] and [AZ99a] (extended version) develop a calculus of module systems, whose syntax, reduction semantics and type system are parametric on the underlying core calculus. Confluence and subject reduction are established, and a subtyping relation on module types is proposed. [TOPIC B]
Furthermore, we have developed Jam, an extension of Java supporting *mixins*, i.e. parametric heir classes [ALZ00]. The implementation is available from http://www.disi.unige.it/person/LagorioG/jam/. [TOPIC B]
[MP99] provides a better understanding of monadic encapsulation of computational effects (namely state), in particular it proposes a more natural encapsulation construct exploiting higher-order kinds, and establishes type-safety in higher-order lambda-calculus (rather than weaker type systems, such as ML or Haskell). [TOPIC B and D]
[CMT00] extends further the work on MetaML to ensure safe multi-stage programming, in particular it proposes a type system to ensure safe use of multi-stage programming constructs in the presence of computational effects (namely ML-like references). [TOPIC B and E]
[CIO00 investigates extensions of Hoare Logic to imperative languages with pointers, giving axioms for constructs for allocating and disposing of memory. The main result is that those axioms express the weakest precondition of the respective commands, hence are relatively complete in the sense of Cook. [TOPIC A]
[MBJ99] investigates the interaction between computational effects (formalised by monads) and datatypes (formalised by functors shapely over lists), in particular it identifies a polytypic combinator, called traversal, which embodies the interaction, and can be used to define combinators, which are more directly usable for generic programming.
[CR99] 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. Among others, [R99] and [RS99] approach the study of realisability models for computation using the point of view of [CR99], and show how the comparison between various hierarchies of type structures relies on logical properties of the basis of the structure itself. In particular, it shows that some intensionally defined type structures are the same as others defined extensionally. [TOPIC D]
[FR99] 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]

References

[AZ99] D.Ancona, E.Zucca. A Primitive Calculus for Module Systems. PPDP'99, LNCS 1702, Springer Verlag, 1999.
[AZ99a] D.Ancona, E.Zucca. A Calculus of Module Systems. Technical Report, DISI, DISI-TR-99-09. Submitted for journal publication, December 1999.
[ALZ00] D.Ancona, G.Lagorio, E.Zucca. Jam: A Smooth Extension of Java with Mixins. To appear in ECOOP'00, LNCS, Springer Verlag, 2000 (DISI-TR-99-15).
[CMT00] C.Calcagno, E.Moggi, W.Taha. Closed Types as a Simple Approach to Safe Imperative Multi-Stage Programming. To appear in ICALP'00, LNCS, Springer Verlag, 2000.
[BMTS99] Z.Benaissa, E.Moggi, W.Taha, T.Sheard. Logical Modalities and Multi-Stage Programming. IMLA, FLoC'99 Workshop, 1999.
[MBJ99] E.Moggi, G.Belle', C.B.Jay. Monads, Shapely Functors and Traversals. CTCS '99, Elsevier, ENTCS 29, 1999.
[MP99] E.Moggi, F.Palumbo. Monadic Encapsulation of Effects: a Revised Approach. HOOTS '99, Elsevier, ENTCS 26, 1999.
[RS99] G. Rosolini, T.Streicher. Comparing models of higher type computation. In L. Birkdedal, J. van Oosten, G. Rosolini, D.S. Scott, eds., Workshop on Realizability Semantics and Applications, 1999, Electr. Notes in Theo. Comp. Sci., Elsevier Science.
[CIO00] C.Calcagno, S.Ishtiaq, P.W.O'Hearn. Semantic Analysis of Pointer Alising, Allocation and Disposal in Hoare Logic. Submitted, March 2000.
[FR99] M.Fiore, G.Rosolini. Domains in H. to appear in Theo.Comp.Sci.
[R99] G.Rosolini. Equilogical spaces and filter spaces. to appear in R.Betti, A.Carboni, F.W.Lawvere, eds., Perugia studies in category theory, algebra and logic.
[CR99] A.Carboni, G.Rosolini. Locally cartesian closed exact completions. to appear in J.Pure Appl. Alg.

Visits

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

K.Fisher visited Genova (24/04/2000 - MURST funding)
S.Drossopoulou visited Genova (23-26/02/2000 - MURST funding)
E.Moggi visited UTS (06-20/02/2000 - MURST and ARC funding)
C.Calcagno visited QMW (01/12/1999-31/03/2000 - Genova and QMW funding)
W.Taha visited Genova (20/12/1999-06/01/2000 - MURST and Chalmers funding)
Robinson visited Genova (15/07-07/08/1999 - QMW funding)
E.Moggi visited OGI (10-25/07/1999 - MURST and OGI funding)
W.Taha visited Genova (02-16/04/1999 - MURST and OGI funding)
Rosolini visited Munich (06-12/04/1999 - APPSEM and German funding)