Genova - Fourth year Progress Report
Researchers: E.Moggi, G.Rosolini, E.Zucca, D.Ancona.
PhD students: C.Calcagno, S.Fagorzi, G.Lagorio, L.Paolini.
- [ALZ01b] is a revised version of [ALZ00a] (see the Third Year Report).
- [AADDGZ01] and [AADDGZ02] present two translations from Fickle (a Java-like language allowing objects that can change their class at
run-time) into plain Java. Both translations are proved to preserve
the static and the dynamic semantics of the language; furthermore,
translation defined in [AADDGZ02] is type preserving.
- [CYO01] shows undecidability for a spatial logic for mutable data
structures, defines several decidable fragments and studies their
complexity with respect to validity and model-checking. [TOPIC A]
- [ALZ02] is an enhanced version of [ALZ01] (see the Third Year Report).
- [ALZ02a] is an enhancement of [ALZ01a] (see the Third Year Report).
It defines an abstract framework for specifying Java compilation schemata,
that is, different possibilities for performing the overall process of Java
compilation. In particular, it focuses on three different schemata:
minimal, SDK and safe, which correspond to a minimal set of checks,
the checks performed by the SDK implementation, and all the checks needed to
prevent run-time linkage errors, respectively.
- [ALZ02b] defines a type system modeling true separate compilation for a small
but significant Java subset, in the sense
that a single class declaration can be intra-checked and compiled
providing a minimal set of type requirements on missing classes.
- [AG02] investigates a possible implementation of the type system proposed in
[ALZ02b]. The proposed algorithm is sound but not complete w.r.t. the
formalization given in [ALZ02b]; however,
a complete implementation is proved to be an NP-hard problem,
while the proposed algorithm exhibits a polynomial time complexity.
- [AZ02] is an enhanced version of [AZ99a] (see the Second Year Report).
- [AZ02a] is an enhanced version of a previous work of D.Ancona and E.Zucca
on axiomatic semantics of mixin modules.
- [CMS??] proposes a type system for a meta-programming language
with references. It uses closed types and a binder for useless
variables. The resulting language is a conservative extension of an
imperative subset of SML. [TOPIC B and E]
- [MS01] 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]
- [FMP01a] proposes an extension of KLAIM (Kernel Language for
Agents Interaction and Mobility) with polymorphism like in system F,
and global types. Values of global types can can freely move over the
network, while values of local types are confined to the locality
where they have been created. Therefore, global types provide, in the
context of distributed computing, an encapsulation mechanism similar
to monadic encapsulation of state. [TOPIC B]
- [FMP01b] extends KLAIM with the types and constructs for
meta-programming proposed in [CMS??]. [FMP01c] introduces MetaKLAIM,
which extends the kernel language of [FMP01a] with MetaML staging
constructs. Since MetaKLAIM require dynamic type-checking, [FMP01c]
uses a type system without closed types, which is simpler but less
accurate. [TOPIC B and E]
- [RR01] characterizes when a realizability interpretation determines a
model of (im)predicative type theory, by determining precisely which
properties the base category C must satisfy in order that the exact
completion of the F-construction on C give a locally cartesian closed
category or a topos. [TOPIC D]
- [FR01] gives a internal description of the category of omega-complete
posets and omega-continuous functions in the model H of Synthetic
Domain Theory. It follows that the omega-cpos lie between the two
extreme synthetic notions of domain given by repleteness and
well-completeness, supporting the point of views that the categorical
intuition and the logical intuition match very closely. [TOPIC D]
In [PR??] the notion of solvability in the call-by-value
lambda-calculus is defined and completely characterized, both from an
operational and a denotational point of view. The operational
characterization is given through a reduction machine, performing the
classical beta-reduction, according to an innermost strategy. Indeed,
it turns out that the call-by -value reduction is too weak to capture
the solvability property of terms. The logical characterization is
given through an intersection type assignment system, assigning types
of a given shape to all and only the call-by-value solvable terms.
- [CHT02] 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]
- [ALZ01b] D.Ancona, G.Lagorio, E.Zucca. A Core Calculus for Java Exceptions.
- [ALZ02] D.Ancona, G.Lagorio, E.Zucca. Jam - Designing
a Java Extension with Mixins.
Submitted for journal publication, March 2002.
- [ALZ02a] D.Ancona, G.Lagorio, E.Zucca.
A Formal Framework for Java Separate Compilation. ECOOP 2002. To appear.
- [AADDGZ01] D.Ancona, C.Anderson, F.Damiani, S.Drossopoulou, P.Giannini, E.Zucca.
An Effective Translation of Fickle into Java. ICTCS 2001.
- [AADDGZ02] D.Ancona, C.Anderson, F.Damiani, S.Drossopoulou, P.Giannini, E.Zucca.
A type preserving translation of Fickle into Java. ENTCS 2002.
- [ALZ02b] D.Ancona, G.Lagorio, E.Zucca. True Separate Compilation of Java Classes.
Technical report. January 2002. Submitted for publication.
- [AZ02] D.Ancona, E.Zucca. A Calculus of Module Systems.
Journal of Functional Programming, 2002.
- [AZ02a] D.Ancona, E.Zucca. A Theory of Mixin Modules:
Algebraic Laws and Reduction Semantics. Mathematical Structures in Computer Science, 2002.
- [AG02] D.Ancona, G.Lagorio. Supporting True Separate Compilation in Java:
A Modular Approach. Technical Report. April 2002. Submitted for publication.
- [CHT02] C.Calcagno, S.Helsen, P.Thiemann. Syntactic Type Soundness
Results for the Region Calculus. In Information and Computation Vol.
- [CMS??] C.Calcagno, E.Moggi, T.Sheard. Closed Types for a
Safe Imperative MetaML. Submitted, November 2001.
- [CYO01] C. Calcagno, H. Yang, P. W. O'Hearn. Computability and
Complexity Results for a Spatial Assertion Language for Data Structures.
In FSTTCS, LNCS, 2001.
- [FMP01a] G.Ferrari, E.Moggi, R.Pugliese,
Global Types and Network Services,
ConCoord Workshop (Lipari),
ENTCS 54, July 2001.
- [FMP01b] G.Ferrari, E.Moggi, R.Pugliese,
MetaKlaim: Meta-Programming for Global Computing (Position Paper),
SAIG Workshop (Florence),
LNCS 2196, September 2001.
- [FMP01c] G.Ferrari, E.Moggi, R.Pugliese,
Higher-Order Types and Meta-Programming for Global Computing,
TOSCA Workshop (Udine),
ENTCS 62, November 2001.
- [FR01] M.Fiore, G.Rosolini,
Domains in H,
Theoret. Comput. Sci., 264, 2001, 171-193
- [MS01] E.Moggi, A.Sabry, Monadic Encapsulation of Effects: A Revised
Approach (Extended Version), Journal of Functional Programming 11(6),
Paolini, L., Ronchi della Rocca, S.
Theoret. Inf. Appl., to appear
- [RR01] E.P.Robinson, G.Rosolini,
An abstract look at realizability,
In Computer Science Logic '01, Ed. L. Fribourg,
Lectures Notes in Computer Science, 2142, 2001, 173-187