Program requirementsCC+examen
TeacherLorenzo Tortora de Falco
Years Master Logique Mathématique et Fondements de l'Informatique

Syllabus

Around the middle of the eighties of the last century, when thanks to the Curry-Howard correspondence the field of research at the crossroads of theoretical computer science and demonstration theory was booming, Jean-Yves Girard introduced and studied denotational models of the system F. He then discovered a very simple model of F, the coherent spaces, which possess remarkable duality properties, and that the connectors of intuitionistic logic can be decomposed by means of more elementary operations in this model. Moreover, it turns out that this decomposition can be internalized through new logical connectors: this is how Linear Logic appears, as the underlying structure of "logic" in general, and of computational processes. Linear Logic is a powerful tool to analyze and control the use of resources in logic and computer science. Its nature as the underlying structure of logic has led researchers to develop techniques, approaches and methods that have been applied in many other fields (sequentiality theory, Scott semantics, lambda-calculus, game semantics, analysis of classical logic and its computational content, implicit complexity, verification, etc.).

The course will present some fundamental tools of proof theory of linear logic. They will be introduced on the basis of the questions that led to their development and we will try to highlight the perspectives opened up by their properties.

Contents

The order in which the different notions will be approached, as well as the progress of the course, will be established in agreement with the teachers of the course "Proofs and Programs: Classical Tools" which takes place during the same semester.

Part I) Introduction

  • coherent spaces and Linear Logic: a brief overview of the history of the invention of Linear Logic
  • Linear Logic as a logical system: calculus of sequents, focusing and reversal, polarization, remarkable fragments.

Part II) Demonstration networks

  • the multiplicative fragment: correction criteria, elimination of cuts, interpretation in frame models
  • the multiplicative and exponential fragment: correction criteria, interpretation in frame models, confluence, strong normalization (syntactic proof and semantic proof)
  • quantifiers in networks
  • the complete system of networks for Second Order Linear Logic
  • the question of separation in networks: behavior of the coherent model and the relational model
  • differential Linear Logic as a refinement of Linear Logic: differential networks, Taylor expansion of a proof network
  • inversion of the Taylor formula and use of differential networks to separate the different interactive behaviors of demonstration networks.

Part III) Two examples of the use of Linear Logic in proof theory

  • Linear Logic as a tool to extract the computational content of classical proofs: interest and stakes of the extension of the Curry-Howard correspondence to classical logic, the Danos-Joinet-Schellinx method of decorations, plunges of classical logic into Linear Logic
  • a logical point of view on bounded time: Girard's method in the search for a logical system with elimination of cuts in "intrinsically" bounded time, the elementary Linear Logic ELL and the Light Linear Logic LLL/SLL, syntactic and semantic characterizations of bounded time.

Bibliography

• Handbook of Linear Logic (available at he address: https://ll-handbook.frama.io/ll-handbook/main.pdf)
• J.-Y. Girard : Linear Logic (Theoretical Computer Science, Vol 50, no 1, pp. 1–102, 1987)
• J.Y. Girard, Y. Lafont, P. Taylor: Proofs and Types (Cambridge University Press, 1989)