People

Research activity in 1999

The research activity of the group has been focused in the development of the projects " Types for Proof and Programs " and " Metodi costruttivi in Topologia, Algebra e Analisi dei Programmi " (see below).

The main goal of the project "Types for Proof and Programs" is the study, development ad experimentation of the systems for proofs and program verification based on type theory. The activity of the Turin group in the 1999 has been on the methods and algorithms for optimization of programs extracted from correctness proofs. A main topic in this field is that of optimization of the functional programs extracted from formal proof which always contains a lot of redundant code corresponding to the parts of the proof which have no computational meaning. In this field the Turin group has already given significant contributions with the work of Berardi, Coppo, and Damiani. Starting from an algorithm described in Damiani's Phd thesis (February 1998), a prototypical tool for removing useless-code from programs written in (a subset of) the functional language Objective CAML has been implemented and is now used for experiments. Moreover, the useless-code elimination algorithm has been extended to languages with algebraic datatypes [3]. This allows to perform more substantial program optimizations transforming and simplifying the data types structure.

In the project about "Metodi costruttivi in Topologia, Algebra e Analisi dei Programmi" the Turin group is involved in two subtasks: program analysis and constructive contents of classical proofs.

Program analysis concerns the study of compile-time techniques for collecting informations about the values and/or behaviours that can arise at run-time. The main goal is both to develop systems for formal reasoning about programs and to define algorithms for program transformation and optimization. This can often be done utilizing methods of constructive logic and in particular of type theory. Further perspectives of program analysis are in software validation and security, such as prevention of malicious behaviours in software components from information networks.

A new model for mobile processes based on notions from type theory has been developed [1]. Its constructive nature should make it useful as a tool for better understanding this interesting class of processes. Moreover a thorough study of the type inference systems for the study of strictness properties has been done and is now in course of publication.

The interest of our group in the field of constructive Proof-Theory focuses mainly on the programming-with-proofs paradigm, consisting in interpretations of formal systems and formal proofs. More precisely we are concerned with methods to obtain actual programs out of formal proofs, both in non-classical and in classical logic. With the aim of studying the constructive content of classical proofs, Berardi and de'Liguoro [2] built a game model where plays may have transfinite length, based on some previous work by Coquand, and used it to show that the no counterexample interpretation of the comprehension axiom of analysis is interpreted by a (transfinite) strategy. The main property of such strategies is that they are "continuous" over continuous, and effective over effective arguments.

1999 Publications

Journals

F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. A filter model for mobile processes. Mathematical Structures in Computer Science, 9(1):63-102, 1999. [1]

Lecture Notes in Computer Science

S. Berardi and U. de' Liguoro. Total functionals and well-founded strategies. In Proceedings of Typed Lambda Calculi and Applications (TLCA'99), volume 1581, Lecture Notes in Computer Science, p. 54-68, Springer, 1999. [2]

F. Damiani. Useless-code detection and elimination for PCF with algebraic Datatypes. In Typed Lambda Calculi and Applications'99, LNCS 1581, pages 83-97. Springer, 1999. [3]

Software Products

Activity and role in the scientific community

• Referee for the Volume of Selected Papers of international Workshop:
  
  • TYPES'98, Lecture Notes in Computer Science, Springer--Verlag.
  
  
• Referee for the international Conferences:
  
  • Typed Lambda Calculi and Applications'99 [2 papers],
  
  
  • Foundations of Software Science and Computation Structures'00 [2 papers].
  
  
• Referee for the Ph.D. dissertation of Dr. Ivano SALVO (Univ. ``La Sapienza'').

• Referee for the international Journal:
  
  • Mathematical Intelligence.
  
  
• Referee for the Volume of Selected Papers of international Workshop:
  
  • TYPES'00, Lecture Notes in Computer Science, Springer--Verlag.
  
  
• Referee for the international Conferences:
  
  • Logic In Computer Science'99 [3 papers],
  
  
  • Computer Science Logic '99,
  
  
  • Conference on Automated Deduction'99
  
  
  • Typed Lambda Calculi and Applications'99.
  
  
• Referee for the Ph.D. dissertation of:
  
  • Dr. Bruno BARRAS (Univ. Paris VII),
  
  
  • Dr. Paul GASTIN (Univ. Paris VII),
  
  
  • Dr. Samir FARKH (Univ. de Savoie),
  
  
  • Dr. Frederic PROST (ENS Lyon).
  
  

• Referee for the international Journal:
  
  • Theoretical Computer Science.
  
  
• Referee for the international Conferences:
  
  • Logic In Computer Science'99,
  
  
  • Static Analysis Symposiom'99,
  
  
  • Foundations of Software Science and Computation Structures'00.
  
  

Oral presentations in Congresses and Conferences

• Invited speaker at the international Conference:
  
  • Typed Lambda Calculi and Applications 1999 (TLCA'99). L'Aquila, 6-9 April 99.
  
  
  • “From filter models to abstract domains”, talk given at the international Workshop on Static Analysis and Types, 17-18 May 1999, Padova.
  
  

• “Useless-code detection and elimination for PCF with algebraic Datatypes”. Typed Lambda Calculi and Applications 1999 (TLCA'99) L'Aquila, 6-9 April 99.


• “Detecting and removing useless-code in functional languages with algebraic datatypes”, talk given at the international Workshop TYPES'99 (meeting of the ESPRIT Working Group 21900 - TYPES), Lokeberg, Sweden, 12-16 June, 1999.


• “Useless-code detection and elimination for PCF with algebraic data-types”, talk given at the international Workshop on Static Analysis and Types, 17-18 May 1999, Padova.