University of Torino

S. Berardi and L.Boerio defined a semantic for an extension of CC with subtyping suitable to distinguish computational and non computational parts of a proof. A by-product of this work is an improved marking system for optimizing programs extracted from proofs in Coq. Berardi and Boerio continued also in their work on program extraction.

S. Berardi and F. Barbanera worked in experiments with program extraction technique for classical logic. The results fo this work are reported in a paper, published in the TACS '97 proccedings, which is based on a lambda calculus + exit formalism,

F. Damiani is finishing his Ph.D. thesis, carried on under the supervision of Prof. M. Coppo, about optimizing programs extracted from proofs, and more in general optimization of typed functional program. The final version of the thesis is expected by the end of the year. On the same subject F. Damiani has written joint papers with F. Prost of the Lyon site and with M. Coppo and P. Giannini.

REFERECES

S. Berardi, L. Boerio: "Minimum Information Code in a Pure Functional Language with Data Types." Proc. of TLCA 97, Nancy, France, LNCS 1210, Springer Verlag 1997.

F. Barbanera, S. Berardi, M. Schivalocchi "Classical" Programming-with-Proofs in lambda-sym: An Analysis of Non-Co nfluence" Proceedings of TACS '97, Japan, LNCS 1281, Springer Verlag 1997.

S. Berardi, L. Boerio : "Program optimization in the calculus of constructions extended with Subtyping" Internal Report, Univesity of Turin, 1997.

M. Coppo, F. Damiani and P. Giannini. "On Strictness and Totality." In International Symposioum TACS'97, LNCS 1281, Springer, 1997.

F. Damiani and F. Prost. "Detecting and Removing Dead Code using Rank 2 Intersecion." In International Workshop TYPES'96 (Selected Papers), LNCS, Springer, to appear.