Genova - Fourth year Progress Report

Achievements

Topic A

• [ALZ01b] is a revised version of [ALZ00a] (see the Third Year Report). [TOPIC A]
• [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. [TOPIC A]
• [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]

Topic B

• [ALZ02] is an enhanced version of [ALZ01] (see the Third Year Report). [TOPIC B]
• [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. [TOPIC B]
• [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. [TOPIC B]
• [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. [TOPIC B]
• [AZ02] is an enhanced version of [AZ99a] (see the Second Year Report). [TOPIC B]
• [AZ02a] is an enhanced version of a previous work of D.Ancona and E.Zucca on axiomatic semantics of mixin modules. [TOPIC B]
• [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]

Topic D

• [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. [TOPIC D]

Topic G

• [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]

References

• [ALZ01b] D.Ancona, G.Lagorio, E.Zucca. A Core Calculus for Java Exceptions. OOPSLA 2001.
• [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. To appear.
• [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. 173, 2002.
• [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), November 2001.
• [PR??] Paolini, L., Ronchi della Rocca, S. Call-by-value solvability, 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