In the year 2002 the research has been focused on the study of type systems, also aimed at the formal analysis and verification of programs, in functional or object oriented languages. A rather fundamental study on the role of types in languages with concurrency and mobility has also been carried on. In this context our work has been carried on along the following lines:

A - Development of type systems tailored for program analysis, strictness and totality analysis in particular.

B - Development of operational models and type systems for the investigation of advanced features of object-oriented programming languages.

C - Investigations on the applicability of the filter model construction to calculi of mobility

D - Investigations on model of fundamental typed calculi for programming languages

A - The paper [CDG02] present type inference system tailored for proving strictness and totality properties of functional languages and, in particular, of the lambda-calculus. Soundness and completeness properties of the type assignment systems for both strictness and totality are proved. The paper also discuss issues related to the interactions of the two analyses.

B - In the paper [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. Suitable type systems are designed to assure consistency and to check correctness of the new construct. An experimental implementation of a version of JAVA enriched with the new primitives is presented in [AADDGZ02] via a translation in standard JAVA.

From another point of view the paper [BDG02] is basic study of the object-based representation of environments for modeling "environment-aware" computations. Correspondence between capabilities of different environments is proved via a notion of bisimulation.

C - The filter model construction allows to define denotational models out of suitable type systems. In the paper [CD02a] a first attempt of applying this construction to calculi suitable to represent mobility is done. The main result is the definition of a fully abstract model for an extension of the basic Ambient Calculus. In [CD02b] this construction is extended to a richer calculus in which communication of higher order processes is allowed. A further extension to system with coactions, like Safe Ambients, is reported in "I. Margaria and M. Zacchi. A filter model for safe ambients. Internal report, December 2002". In this report a refined notion of type, representing a process trace, is Introduced.

D - In [BeBe02] it is shown that Friedman's proof of existence of non-trivial beta-eta-complete models of lambda-calculus can be extended to system F. We isolate a set of conditions which are sufficient to ensure beta-eta-completeness for a model of F and we discuss which class of models we get.

In [BaBe02] the authors define a model of the second-order lambda calculus (F system) in which polymorphic maps are interpreted by generic continuous maps, that is, maps really depending on input types. The model is a Scott domain, representing the class of types, whose elements are themselves Scott Domains.