Genova - Third year Progress Report
Researchers: E.Moggi, G.Rosolini, E.Zucca, D.Ancona.
PhD students: C.Calcagno, G.Lagorio, L.Paolini.
- [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]
- [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]
- [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]
- [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]
- [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
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
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
- [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
- [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
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)