The research topic of the group is to build abstract models for reasoning about the semantics of programming languages, and then to develop formal tools, based on the semantics, for proving properties of programs. In particular, the semantics techniques are developed for paradigmatic languages based on the lambda calculus, modelling different kinds of computation.

The results obtained by the group in its activity in the year 2002 are sommarized in what follows.

In the area of the operational semantics:

- An extension of lambda calculus for which the Berarducci trees equality coincides with observational equivalence has been built [1].

• The existence of an infinitary confluent and normalising extension of the finite extensional lambda calculus with beta and eta reduction has been proved [6].

In the area of the denotational semantics:

- an extension of lambda calculus which is fully abstract for Scott's D-infinity-models has been presented. This language is an infinitary lambda calculus which not only has the confluence property, but also is normalising: every term has its infinite-eta-Bohm tree as unique normal form [5]

- A PER model in a D-infinity domain has been studied, through intersection types. The PER inclusion, modelling the subtyping relation, is intepreted as inverse inclusion of propositional theories, so exhibiting an isomorphism between the two presentations [2].

In the area of logical tools for studying programming languages properties:

- The problem of designing a machine-independent characterization of polinomial computations has been studied, starting from LAL, a restriction of the Linear Logic characterizing this computational class. A preliminary result is showed in [4].

- A typed lambda calculus with intersection types has been designed, starting from the Intersection Logic [3]. The interest of such a language leads in its intrinsic parallel operational behaviour.

- A theory of specifications based on the Calculus of Inductive Constructions has been presented in [7]. It internalizes the notion of realizability and the process of program extraction by means of a reduction relation.

- A subset of the theory of specifications where we only consider data types and propositions has been studied in [8]. A counterexamples for Subject Reduction and Strong Normalization properties are presented.

- In [9] the theory of specifications in the context of the calculus of constructions is studied. In particular the Subject Reduction and Strong Normalization properties are proved, by restricting the beta-reduction.

- In [10] the notion of ultra-sigma type is introduced. Several theories for program extraction can be expressed through pure type systems with ultra-sigma types. In this way it is possible to give a description of the process of program extraction which is independent of the type lambda calculus we choose.