Research activity in 1998
The research of the group in 1998 focused on four main directions: program analysis and tranformations, proof theory, semantics of programming languages, and type systems.
The area of program analysis concernes the study of compile-time techniques for collecting informations about the value and/or behaviours that can arise at run-time. The main goal is both to develop systems for reasoning formaly about programs and to define algorithms for program transformation and optimization. Further perspectives of program analysis are in software validation and security, such as prevention of malicious behaviours in software components from information networks.
The approach of our group is based on constructive logics and type theory. We work mainly on "inference based" program analysis, but we do not disregard model theoretic approaches and techniques, like "abstract interpretation. We have developed inference systems for reasoning about strictness, totality and dead-code properties for higher-order functional programming languages. We also have proposed simplification techniques expecially suited for programs extracted from formal proofs in logical frameworks (like Coq).
The interest of our group in the field of proof theory focuses mainly on the programming-with-proof paradigm, consisting in interpretations of formal systems and formal proofs. More precisely we are concerned with methods to obtain actual programs, if any, out of formal proofs, both in intuitionistic and in classical logic. Program extraction from intuitionistic proofs rests on a firm and solid rock, thanks to several and well-known results. However much has still to be done in order to turn the theoretical results into tools for actual programming. Results obtained by our group are in this direction, expecially about code optimization for programs automatically extracted from formal proofs.
The use of classical proofs for programming purposes is more challenging. We have built over known methods, using either logical reduction rules (like Prawitz's reductions), or reductions inspired by those for continuation-based calculi. But we have also proposed a completely new natural deduction system and a set of reductions which try to exploit the inner symmetricity of classical logic. Concerning the foundations of extraction of the computational content out of classical proofs we propose a game-theoretic semantics and a proof interpretation based on recursive functionals, which clarifie and improve over Kreisel's no-counterexample interpretation.
In the area of semantics of programming languages, to encompass computational models closer to actual programming languages, we study, through intersection types, models of call-by-value lambda-calculus, both in the category of Scott's domains and of coherent spaces. All these constructions turn out to be particular cases of a categorical definition of models for this calculus.
We have also considered lambda-models induced by extensions of the intersection type discipline obtained by allowing infinite intersections and by defining intersection as a partial operator. Moreover, we added the union type constructor, obtaining a powerful tool to describe models of the lambda-calculus, of its extensions with non-deterministic choice and a parallel operators, and of the pi-calculus as well as higher-order process calculi. These studies provide foundations for "inference based" program analysis, and are currently under development in view of applications to concurrent and object-oriented programming languages.
The interst of our group in the field of type systems focuses mainy on the study of type systems for functional and object-oriented languages. The theoretical basis is the theory of Curry type assignment system for pure lambda-calculus, whose extension with intersection types has been one major concern of the group in the '80.
The study of several systems obtained by adding to the intersection types universal quantification, recursion, union and existential quantification has been, and still is, one of the principal aims of the group. Proof theoretical properties of these systems have been established and put to use, e.g. in the search of typing algorithms, mainly based on the notion of principal type scheme. A systematic investigation of type assingment systems obtained from strongly typed calculi via erasing functions has been pursued. A cube of assignment systems, mirroring the Barendregt's cube of typed lambda-calculi, has been defined. Subject reduction and strong normalization theorems for terms typable in such assignment systems have been established.
We studied various assignment systems for extended lambda-calculi modeling basic features of OO languages.
1998 Publications
M. Dezani-Ciancaglini, M. Takahashi, M. Okada (Eds.). MSJ-Memoir Vol. 2 ``Theories of Types and Proofs''. Mathematical Society of Japan, pages. 295, 1998.
S. Berardi S. Baratella. Constructivization via Approximation and Examples. In MSJ-Memoir Vol. 2 "Theories of Types and Proofs''. Mathematical Society of Japan, 177- 205, 1998.
M. Coppo, F. Damiani, and P. Giannini. Inference based analysis of functional programs: dead-code and strictness. In MSJ-Memoir Vol. 2 ``Theories of Types and Proofs''. Mathematical Society of Japan, 143- 176, 1998.
M. Dezani-Ciancaglini, E. Giovannetti, and U. de' Liguoro. Intersection types, lambda-models and Böhm trees In MSJ-Memoir Vol. 2 ``Theories of Types and Proofs''. Mathematical Society of Japan, 45- 97, 1998.
F. Alessi, M. Dezani-Ciancaglini, and U. de' Liguoro. A convex powerdomain over lattices: its logic and lambda -calculus. Fundamenta Informaticae, , 32 (3-4);193-250,1998.
S. Berardi. Intuitionistic completness for first order classical logic. Journal of Symbolic Logic, to appear.
S. Berardi S. Baratella. Approximating classical theorems. Journal of Logic and Computation, 8(6):839-854,1998.
S. Berardi, T. Coquand, M. Bezem. On the constructive content of the axiom of choice. Journal of Symbolic Logic, 68(2):600-623,1998.
M. Dezani-Ciancaglini, U. de' Liguoro, and A. Piperno. A filter model for concurrent lambda-calculus. Siam Journal on Computing, 27(5):1376-1419, 1998.
F. Honsell, A. Pravato, and S. Ronchi della Rocca. Structured operational semantics of a fragment of the language scheme. Journal of Functional Programming, 8(4):335-365,1198.
F. Barbanera, M. Dezani-Ciancaglini, and F.-J. de Vries. Types for trees. In Proceedings of PROCOMET '98, pages 11-29. Chapman & Hall, London, 1998.
V. Bono and K. Fisher. An Imperative First-Order Calculus with Object Extension. In ECOOP '98. Springer-Verlag, 1998. To appear (a preliminary version appeared in the electronic proceedings of FOOL5, 1998).
M. Coppo. Recursive types: the syntactic and semantic approaches. In Theories of Types and Proofs. Kyoto University, 16-41, 1998.
F. Damiani and F. Prost. Detecting and Removing Dead-Code using Rank 2 Intersection. In International Workshop TYPES'96, Selected Papers, LNCS 1512, pages 66-87. Springer, 1998.
M. Dezani-Ciancaglini, B. Intrigila, and M. Venturini-Zilli. Böhm's Theorem for Böhm Trees. In Proceedings of ICTCS'98, pages 1-23. World Scientific, Oxford, 1998.
F. Damiani. Non-standard type inference for functional programs. PhD thesis TD 4/98, Dipartimento di Informatica, Università di Torino, C.so Svizzera 185 - I 10149 Torino - Italy, 299 pages, February 1998 .