Contributions offered by Eugenio Moggi for topics 
B (program structuring), D (verification methods), E (automatic
program transformation)

1) encapsulation of effects and existential types
   (relevant to topic B and may raise issues for topic D)

Haskell provide encapsulation of effects using a construct
run of type forall X.(forall S.T(S,X))->X.  We propose an
alternative approach which uses universal quantification over
higher kinds and generalizes the encoding of existential types
in terms of universal and functional types.  The simplest
technique to establish correcness of the encapsualation of
effects is based on small step operationa semantics
(see Lauchbury and Sabry ICFP97).  An interesting issue is
the possibility of extending the approach to deal with
incremental encapsulation of effects, however it is not clear
how to formulate correctness of encapsulation in a parametrized
form, nor how to extend the proof techniques.


2) semantics of the multistage programming language MetaML
   (relevant to topic B and E)

I can outline a categorical semantics of MetaML and discuss
what extensions it suggests to MetaML, and the relations with
the work of Davies and Pfenning (explaning various kinds of
multi-level languages in terms of modal and temporal logic)
This is work in progress in collaboration with people at OGI
(T.Sheard, W.Taha and Z. Benaissa).

--------------------------------------------------------------
Result of feedback form submitted by
Moggi (moggi@disi.unige.it) on Wednesday, July 1, 1998 at 18:18:3