Research activity in 2001
In the year 2001 the research has been focused on the study of type systems, also aimed at the for formal analysis and verification of programs, in functional or object priented langiages. In this context our work has been carried on along the following lines:
A - Development of basic formal theory of type systems with recursive operators on types, both on the formal side (study of fundamental properties) and on the pragmatic one (inference algorithms).
B - Development of operational models and type systems for the investigation of advanced features and type systems of object-oriented programming languages.
C - Investigations on the computational content of classical logic.
The paper [1] investigates some basic properties of type system which allows recursive definition of types, a quite useful tool in programming practice. Basic results are the characterization of the relations between strong and weak type equivalence and the proof of existence of principal typings. In [2] a type checker for a typically type free language (the Cuch machine) is presented. This system combines ML-polymorphism, recursive type definitions and subtyping to obtain a quite flexible type system in which also partial type information can be exploited to detect well-formedness properties of untyped programs.
In the papers [4] and [5] is presented an investigation on a new language feature for object oriented programming languages which allows to define objects which can dynamically change class (under some restrictions). 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 [3] via a translation in standard JAVA.
Another activity, carried on mainly by S. Berardi, concerns the study of the constructive contents of classical logic proofs. The main goal of this research is to find methods for extracting programs from classical proofs of their specifications extending to classical logic the well known methods of program extraction developed in intuitionistic type theory. One main point of investigation concerns the view of classical logic in a limiting sense, in the same way real numbers are seen as limits of the rational ones. The programs extracted in this way exhibits interesting concurrent features. This activity has lead to some technical reports which have been submitted to international journals.
Publications 2001
[1] M. Coppo. Type Inference with Recursive Type Equations-Lecture Notes in Computer Science, vol. 2030- pp.184-198 - Springer 2001.
[2] M. Coppo and Daniel Hirschoff. Incremental Inference of Partial Types. Lecture Notes in Computer Science vol. 2202, pp. 50-73, Springer 2001
[3] D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini, and E. Zucca. An effective translation of Fickle into Java. Lecture Notes in Computer Science vol. 2202, pp. 215-234, Springer 2001.
[4] S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini and P. Giannini. Fickle: Dynamic object re-classification. Lecture Notes in Computer Science vol. 2072, pp. 130-149, Springer 2001.
[5] S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini and P. Giannini. Fickle: Dynamic Object Re-classification. FOOL - INT. WORK. ON FOUNDATIONS OF OBJECT-ORIENTED LANGUAGES 2001 London G.B. Electronic proceedings of FOOL8 (http://www.cs.williams.edu/~kim/FOOL/ A
