Genova - Second year Progress Report
Researchers: E.Moggi, G.Rosolini, E.Zucca, D.Ancona.
PhD students: C.Calcagno, G.Lagorio, F.Palumbo.
- [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
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
- [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]
- [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,
- [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,
- [FR99] M.Fiore, G.Rosolini. Domains in H. to appear in
- [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.
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)