People

Research activity in 1997

The research of the group in 1997 focused on three main directions: type systems , logical semantics, and proof theory.

In the area of type systems the study of several systems obtained by adding to the intersection types universal quantification, recursion, union and existential quantification is still one of the principal aims of the group. Proof theoretical properties of these systems have been established and put to use, e.g. in the search of typing algorithms, mainly based on the notion of principal type scheme.

A systematic investigation of type assignment systems obtained from strongly typed calculi via erasing functions has been pursued. A cube of assignment systems, mirroring the Barendregt's cube of typed lambda-calculi, has been defined. Subject reduction and strong normalization theorems for terms typable in such assignment systems have been established.

The investigation in the field of object oriented languages has led to the definition of type systems for extended lambda-calculi modeling basic features of object based languages including notions of subtyping and incomplete objects. In this area we are currently investigating the possibility of infering types.

The dynamic meaning of a program is naturally represented by a tree containing the relevant information which can be extracted by running it. Types are typical static tools to describe properties of programs. In our research we connect static and dynamic aspect of programs on one side by devising powerful typing disciplines, and on the other by considering non-standard type inference systems for typed functional programs.

There are both foundational motivation (develop a theoretical framework for non standard type analysis) and practical ones for the study of non-standard type inference. In particular these systems can be used for the construction of static analyzers and optimizers of functional programming languages. We have investigated properties of inference systems for reasoning about strictness, totality, and dead-code analysis. Semantic properties of these systems (like adequacy and completeness) have been studied via an operational semantics of the underlying language. We have also considered in some detail the possibility of implementations of static analysers based on these systems. In our work we have developed sound and complete inference algorithms for strictness and dead-code analyses.

On the area of logical specification of domains we investigated a fully abstract model for the pi-calculus, that is the extension of the CCS formalism in which the topology of the interaction between processes may change dynamically. The description of the domain through a type assignment system gives also a sound and complete proof system for the properties expressed by types. We also studied a powerdomain functor over lattices, close to convex powerdomain, defining a new functor P over continuous lattices such that "sets" satisfy the key convexity property. This solution is described vie its compact elements, as an algebra directly coming from the definition of P-algebras, and we introduce a lambda calculus such that D comes out to be a fully abstract model of such calculus.

In another direction, we introduced through intersection types different models of call-by-value lambda-calculus, whose domains are Scott's domains as well as coherent spaces. All these models turn out to be particular cases of a categorical definition of models for this calculus.

The interest of the lambda-group of Torino in the field of proof theory has been focused mainly on the so-called programming-with-proofs paradigm. For what concerns classical logic a number of computational interpretations have been studied, among them a game-semantics interpretation and an interpretation based on recursive functionals which clarifies and improves the well-known no-counterexample interpretation by Kreisel. Also a number of methods have been proposed in order to compute with formal proofs. Such methods are based on reduction rules on natural deduction proofs which are in a "propositions-as-proof" correspondence with terms of various lambda-calculi. Some of these methods use already known logical reduction rules (like Prawitz's reductions), some others use reductions inspired by those for continuation-based calculi, while a last one uses a completely new natural deduction system and a set of reductions which try to exploit the inner "symmetricity" of classical logic. By this expression we mean, in general, the use of formal proofs and proof-theoretical methods for computational purposes. For what concerns intuitionistic logic, some results have been obtained in the area of optimization of code of programs extracted from formal proofs. A few optimization algorithms have been developed, together with their correctness proofs, which have been implemented in a few real systems in France and Japan.

We also studied the problem of consistency of analysis. We face this problem pursuing research started by Kreisel, who devised a constructive, but uncomplete, functional interpretation of analysis based on the notion of continous functional. Although we have obtained some interesting results in this area, this work is still in progress.