People

Research activity in 1999

The research topic of the group is to build abstract models for reasoning about the semantics of programming languages, and then to develop formal tools, based on the semantics, for proving properties of programs. In particular, the semantics techniques are developed for paradigmatic languages, based on the lambda calculus, modeling different kinds of computation. The research activity of the group in 1999 followed essentially two lines: one about the construction of semantics tools (inside the MURST project " Tecniche Formali per la specifica, l'analisi, la verifica, sintesi e la trasformazione di sistemi software "), the other about the use of linear logics for modeling properties of programs (inside the TMR project "Linear Logic"). In the first line the following results have been obtained. The so-called "call-by-value lambda calculus" has been studied. The call-by-value lambda calculus is a paradigmatic language which is particularly interesting , which models both the call-by-value parameter passing and the lazy evaluation. While these two features are present in the big part of real programming languages, this calculus has not yet been completely investigated, from a semantic point of view. In [1] Ronchi, Roversi and Pravato gave the first categorical characterization of a model for the call-by-value lambda calculus, which is not complete but powerful enough to catch all the existing models in different settings. Type assignment systems are very powerful tools for reasoning abut properties of programs. The type systems derived from both second order and higher order implicative intuitionistic logic are very powerful. In [2], Ronchi, Kfoury, Tiuryn, and Urzyczyn studied the typability for these systems. They proved that, in the second order case, the typability is preserved by alpha reduction on types (i.e., renaming of universally quantified type variables), while in the last case this is not true. The importance of the result leads in the fact that, in the second order case, type checker and/or type inference algorithms can be implemented without use of renaming, which is an operation difficult to be automatized. The second line of the research activity of the group is about the linear logic. Linear logic is a refinement of the classical one, where the non linear uses of premises are controlled through modal operators. Its interest in the study of programming languages leads in the fact that it can be used for controlling the complexity of both the evaluation and of the use of resources. A further refinement is the Light Linear Logic, and its affine version, which have been defined for characterizing the computations in polinomial time. Roversi, in [3], highlighted a blocking error in the proof of P-time completeness for Light Affine Logic, which was already present in the analogous proof for Light Linear Logic.. He showed how to change the proof to make it working, so conforming the relevance of the two logical systems in the area of Implicit Computational Complexity. Moreover Berardi and de'Liguoro, in [4], used a game semantics approach, whose theoretical justification has been developed starting from Linear Logic, for interpreting the total functionals.

1999 Publications

Journals

A. Pravato, S. Ronchi della Rocca, and L. Roversi. The call by value lambda -calculus: a semantic investigation. Mathematical Structures in Computer Science, 9(5):617-650, 1999. [1]

D. Kfoury, S. Ronchi Della Rocca, J. Tiuryn, P. Urzyczyn. Alpha-conversion and Typability, Information and Computation, 150, (1999),pp.1-21. [2]

Lecture Notes in Computer Science

L. Roversi. A P-Time Completeness Proof for Light Logics. In Ninth Annual Conference of the EACSL (Computer Science Logic, CSL'99), volume 1683 of Lecture Notes in Computer Science, pages 469-483, Madrid (Spain), September 1999. Springer-Verlag. [3]

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

Activity and role in the scientific community

• Member of the Editorial Board of the international Journal:
  
  • ACM Transactions on Computational Logic
  
  
• Member of the Scientific Committee of the group "Logique" of University Paris 7:


• Member of the organizing Committee of the international Conference:
  
  • Logic In Computer Science
  
  
• Co-chair (with Eugenio Moggi) of the international Conference:
  
  • FloC (Trento, luglio 1999).
  
  

• Author of a review (pubblished in the international Journal Mathematical Review) for the paper:
  
  • "A Deterministic Lazy Narrowing Calculus" (by A. Middeldorp and S. Okui).
  
  

• Author of a review (published in the international Journal Mathematical Review) for the paper:
  
  • "The call-by-name lambda calculus" (by J. Maraist, M. Odersky, P. Wadler).
  
  
• Referee for the international Journals:
  
  • Journal of Computing and Information,
  
  
  • Fundamenta Informaticae,
  
  
  • Mathematical Structures in Computer Science.
  
  
• Referee for the international Conferences:
  
  • Logic In Computer Science'99,
  
  
  • Foundamentals of Computing Theory'99,
  
  
  • Typed Lambda Calculus and Applications'99 [2 papers],
  
  
  • Foundations of Software Science and Computation Structures'00.
  
  

Oral presentations in Congresses and Conferences

• Invited speaker at the inaugural Workshop for the research group "Proofs, Programs and Systems" of CNRS and Paris 7 University.


• Invited speaker at the Annual TMR workshop on Linear logic

• Lecturer at the international School:
  
  • School on Logical Relations, Universite` de Savoie, September 1999
  
  
• "Total functionals and well-founded strategies", talk given at Typed Lambda Calculus and Applications 1999 (TLCA'99), L'Aquila, 6-9 April 99.

• Ninth Annual Conference of the EACSL (CSL'99), Madrid (Spain), September 1999.