University of Torino

  Further work has been done on the development of  type based techniques  for detecting and removing dead code from  programs  extracted from proofs  ([1], [2])  and, in general, on the study of program analysis and optimization  techniques based on type inference ([3]).  On the ground of  [1], [2] an  experimental implementation of a program extraction algorithms has been done. We are testing it  on the term produced by the COQ system.  Other  work on type inference algorithms and inference systems in general also been done in [4], [5].
    T. Coquand visited Turin site for a month, in September 1999, working with S. Berardi in game semantic for Classical Mathematical Analysis.   The aim of the research was to define a notion of game validating Choice axiom. This notion of game  produces, by an extraction process, executable programs from proofs of simply existential statements ([8]).
    S. Berardi  continued the cooperation with Ch. Berline (Paris) on the interpretation of polymorphic lambda calculus in continuous model using a two level information systems ([6], [7]).
 

REFERENCES

[1] F. Damiani: " Redundant-code detection and elimination for PCF with algebraic Datatypes."   Proc. of  TLCA '99, Lecture Notes in Computer Science  n.   , Sringer Verlag.
[2]  F. Damiani, P. Giannini: " Automatic dead-code detection and elimination for HOT functional programs. " to appear in  J. Funct. Prog..
[3]  M. Coppo, F. Damiani, P. Giannini: "Strictness, totality, and non-standard type inference."  to appear in Theoret. Comp. Sci..
[4]  F.Damiani. "Typing local definitions and conditional expressions with rank 2 intersection."  Internal report, Dipartimento di Informatica, University of  Turin,  1999.
[5] S. Drossopoulou, M. Dezani-Ciancaglini, F. Damiani,  P. Giannini.
"Objects dynamically changing class". Internal report, Dipartimento di Informatica, University of Turin, 1999.
[6]  C. Berline, S. Berardi: " Beta-eta-complete models for System F" Internal Report, Univesity of Turin, 1998 (submitted  for pubblication to M. F. C. S.).
[7] C. Berline, S. Berardi: " Webbed models for System F " internal Report, Univesity of Turin, 1998 .
[8] S. Berardi, T. Coquand " Transfinite Games" submitted to JSL.
 
 
 
 
   

University of Torino