People

Research activity in 2000

In the year 2000 the research has been focused on the study of type systems for formal verification, analysis and transformation of programs. In this context our work has been carried on along the following lines:

The papers [2] and [4] are in the line A. In [2], Damiani introduces inference algorithms for a type system combining rank-2 intersection types with other fundamental features of higher-+order polymorphic type systems, while [4] presents a generalization of the notion of filter models (a family of models strongly connected with the notion of type) extending the class of representable functions.

The papers [3] and [5], instead, introduce type systems for the detection and the elimination of useless code in functional programming languages. This goal is achieved by defining suitable transformations which preserve the semantics of the language. An implementation of the systems presented in these papers is under development. An introduction of the useless code elimination techniques developed by the Turin group is given in [1].

Another activity, carried on mainly by S. Berardi, concerns the study of higher-order type systems and their use for the automatic synthesis of programs from classical proofs of their correctness. This activity has lead to some technical reports which have been submitted to international journals.