Research activity in 2002

Aim of this group is the study of type systems for functional, concurrent and object-oriented languages. The theoretical basis is Curry type assignment system for pure lambda-calculus and its extensions. The activity in 2002 mainly focused on:

1) types for Java-like languages and (mobile) objects;

2) intersection types for lambda calculi and calculi of explicit substitutions;

3) types for ambient calculi.

Types for Java-like languages and (mobile) objects.

[DDDG02] suggests language features for object reclassification, i.e. an object may change its class membership at run-time. These features extend an imperative, typed, class-based, object-oriented language.

Intersection types for lambda calculi and calculi of explicit substitutions.

[BBDV02] introduces a type assignment system which is parametric with respect to five families of trees obtained by evaluating lambda-terms. Then it proves, in an (almost) uniform way, that each type assignment system fully describes the observational equivalences induced by the corresponding tree representation of terms.

[DL02] illustrates the use of intersection types as a semantic tool for showing properties of the lattice of lambda theories. Relying on the notion of easy intersection type theory it successfully builds a filter model in which the interpretation of an arbitrary simple easy term is any filter which can be described in an uniform way by a predicate.

[GL02] develops a general reducibility method is for proving reduction properties of lambda terms typeable in intersection type systems with and without the universal type. This method leads to uniform proofs of confluence, standardization, weak head normalization of terms typeable in the system with the universal type.

[BD02] characterises the strongly normalising terms of a composition-free calculus of explicit substitutions (with or without garbage collection) by means of an intersection type assignment system.

[DFGM02] compares Meyer and Routley's minimal relevant logic B+ with the recent semantics-based approach to subtyping introduced by Frisch, Castagna and Benzaken

in the definition of a type system with intersection and union types.

Types for ambient calculi.

[BDSS02] presents a bottom-up algorithm which, given an untyped process P, calculates the minimal set of constraints on security levels such that all the actions during a run of P can be performed without violating the security level priorities.

[CD02a] and [CD02b] investigates the possibility of developing filter models for calculi representing mobility. [CD02a] defines a model for a variant of the Ambient Calculus. [CD02b] develops a filter model for an extension of the Ambient Calculus in which processes can be passed as values. Both models turn out to be fully abstract with respect to a notion of contextual equivalence which takes into account the ambients at top level.

2002 Publications

[BBC02] V. Bono, M. Bugliesi, and S. Crafa. Typed Interpretations of Extensible Objects. ACM TOCL 3(4), 2002.

[BBDV02] S. van Bakel, F. Barbanera, M. Dezani-Ciancaglini, and F.-J. de Vries. Intersection types for lambda-trees. Theoretical Computer Science, 272(1-2):3-40, 2002.

[BBV02a] L. Bettini, V. Bono, and B. Venneri. Towards Object-Oriented Klaim. In TOSCA'01, volume 62 of ENTCS. Elsevier, 2002.

[BBV02b] L. Bettini, V. Bono, and B. Venneri. Coordinating Mobile Object-Oriented Code. In COORDINATION'02, LNCS 2315, pages 56-71. Springer-Verlag, 2002.

[BD02] S. van Bakel and M. Dezani-Ciancaglini. Characterising strong normalisation for explicit substitutions. In LATIN'02, LNCS 2286, pages 356-370. Springer, 2002.

[BDG02] V. Bono, F. Damiani, and P. Giannini. A calculus for ``environment-aware'' computation. In F-WAN'02, volume 66.3 of ENTCS. Elsevier, 2002.

[BDSS02] F. Barbanera, M. Dezani-Ciancaglini, I. Salvo, and V. Sassone. A type inference algorithm for secure ambients. In TOSCA'01, volume 62 of ENTCS. Elsevier, 2002.

[BK02] V. Bono and M. Kerber. Crash in Program and Logic. In AVocS 2002, Birmingham, U.K., 2002. Informal Proceedings.

[CD02a] M. Coppo and M. Dezani-Ciancaglini. A fully abstract model for mobile ambients. In TOSCA'01, ENTCS 62. Elsevier Science B. V., 2002.

[CD02b] M. Coppo and M. Dezani-Ciancaglini. A fully abstract model for higher-order mobile ambients. In VMCAI'02, LNCS 2294, pages 255-271. Springer, 2002.

[DDDG02] S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. More dynamic object re-classification: Fickle_II. ACM Transactions On Programming Languages and Systems, 24(2):153-191, 2002.

[DFGM02] M. Dezani-Ciancaglini, A. Frisch, E. Giovannetti, and Y. Motohama. The relevance of semantic subtyping. In ITRS'02, ENTCS, 70.1. Elsevier, 2002.

[DL02] M. Dezani-Ciancaglini and S. Lusin. Intersection types and lambda theories. In Electronic Proceedings of WIT'02 (http://www.irit.fr/zeno/WIT2002/proceedings.shtml), 2002.

[GL02] S. Ghilezan and S. Likavec. Reducibility: a ubiquitous method in lambda calculus with intersection types, ITRS'02, ENTCS, 70.1. Elsevier, 2002.