DIPARTIMENTO   DI   INFORMATICA
Università di Torino

Research Report Year 1998

RESEARCH ACTIVITY

  People   Research Activities   Publications   Software Products   Research Grants

SEMANTICS AND LOGICS OF COMPUTATION

People

Mariangiola Dezani

Full Professor Principal Investigator

dezani(at)di.unito.it

Mario Coppo

Full Professor

coppo(at)di.unito.it

Simonetta Ronchi della Rocca

Full Professor

ronchi(at)di.unito.it

Ines Margaria

Associate Professor

ines(at)di.unito.it

Maddalena Zacchi

Associate Professor

zacchi(at)di.unito.it

Franco Barbanera

Senior Researcher (From Nov. 1, Associate Professor Univ. of Catania)

barba(at)di.unito.it

Stefano Berardi

Senior Researcher (From Nov. 1, Associate Professor Univ. of Lecce)

stefano(at)di.unito.it

Paola Giannini

Senior Researcher (From Nov. 1, Associate Professor Un. Piemonte Orientale)

giannini(at)di.unito.it

Ugo de' Liguoro

Researcher

deligu(at)di.unito.it

Viviana Bono

Ph.D. Student

bono(at)di.unito.it

Ferruccio Damiani

Research Collaborator

damiani(at)di.unito.it

Luca Roversi

Research Collaborator

rover(at)di.unito.it

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 .

Research grants

Title of project

Project leader

Funding Organization

Kind of grant

Esprit Working Group


21900-Types

M. Coppo

European Union

Esprit Working Group

Linear Logic

S. Ronchi della Rocca

European Union

TMR

Typed Lambda Calculus

S. Ronchi della Rocca

European Union

Human Capital Mobility

Formal techniques for specification, analysis, verification, synthesis and transformation of software systems

S. Ronchi della Rocca

MURST

Project of National Interest (ex 40%)

Foundations of Concurrent Language

M. Dezani

Universita' di Torino

ex 60%

Activity and role in the scientific community

Mariangiola Dezani
  • Member of the Program Committee: ICTCS'98, Prato November '98

  • Member of the Editorial Board of Information and Computation

  • Reviewer of International Conferences: Logic in Computer Science 98, ICALP 98, MFCS 98.

  • Reviewer of International Journal Information and Computation, Theoretical Computer Science, Mathematical Review, Journal of Symbolic Logic, Mathematical Structure in Computer Science

Mario Coppo
  • Reviewer of International Conferences: Logic in Computer Science 98, TYPES 98, Computer Science Logic98.

Simonetta Ronchi della Rocca
  • Member of the Program Committee: ICTCS'98, Prato November 98

  • Reviewer of International Conferences: ICTCS 98.

  • Reviewer of International Conferences: Theoretical Computer Science, Mathematical Structure in Computer Science

Ines Margaria
  • Reviewer of International Conferences: LICS 98.

Maddalena Zacchi
  • Reviewer of International Conferences: TLCA 98.

Ugo De' Liguoro
  • Reviewer of International Conferences: Logic in Computer Science 98.

  • Reviewer of International Journal: Theoretical Computer Science, Mathematical Review, Fundamenta Informaticae, Mathematical Structure in Computer Science

Paola Giannini
  • Reviewer of International Conferences: ICTCS 98, SAS98, LICS98.

  • Reviewer of International Conferences: Information and Computation

Viviana Bono
  • Reviewer of International Conferences: ACM Conference on Principles of Database Systems 1998

  • Reviewer of International Conferences: Information and Computation.

Ferruccio Damiani
  • Reviewer of International Conferences: Software Seminar '98 (SOFSEM'98),

Oral Presentations in Congresses and Conferences

Stefano Berardi
  • Workshop on Linear Logic- September 98 (Tenda)

Viviana Bono
  • FOOL'98 (San Diego (U.S.A.),

  • Workshop NATO "Foundations of object-oriented, functional and parallel programming" Varsavia

Mario Coppo
  • Workshop TYPES "Type inference approach to program properties", Chambery April 98.

Ugo de’Liguoro
  • Workshop TYPES Marsiglia,

  • Workshop NATO "Foundations of object-oriented, functional and parallel programming" Varsavia

Mariangiola Dezani
  • Conference ICTCS'98, (Prato November 98)

  • Conference PROCOMET '98

Simonetta Ronchi Della Rocca
  • Conference on Unification- June 98 (Roma) "Curry Howard isomorphism for type assignment systems"

  • Workshop on Linear Logic- September 98 (Tenda) "Lambda Calculus and Intuitionistic Linear Logic"

Department home [Information] [People] [Research] [Ph.D.] [Education] [Library] [Search]
[Bandi/Careers] [HelpDesk] [Administration] [Services] [Hostings] [News and events]

Administrator: wwwadm[at]di.unito.it Last update: May 17, 2018