Description

This school is mainly directed towards Master's students with a background in logic and philosophy, computer science or mathematics. It is also open to PhD students and researchers who would like to learn about linear logic.

The goal is to give a structured introduction to the main concepts and results in linear logic. It will assume as prerequisites only a basic knowledge of classical logic and of formal proof systems (sequent calculus and natural deduction). The aim is to allow the participants to understand, in particular, the motivations and origins of linear logic, its logical connectives, sequent calculus, proof-nets, semantics, relationships with intuitionistic and classical logic etc. The lectures will be given in English.

The presented material will allow the participants to follow the workshops organized on the following days.

Speakers and Material

• Jean-Baptiste Joinet
  • Introduction
• Olivier Laurent
  • Multiplicative Linear Logic
  • Exercises
• Damiano Mazza
  • Attack of the Exponentials
  • Exercises
• Lionel Vaux
  • Denotational Semantics of Linear Logic
  • Exercises

Localization

The school will take place in amphi Huvelin de l'Université Lyon 3.

Program

Prerequisites

We strongly suggest some practice on sequent calculus using the online interactive tutorial.

Content

• Introduction
• The multiplicative fragment of Linear Logic
  
  • proof-nets
  • sequent calculus
  • cut
  • relational model
• Exponential connectives
  
  • proof-nets with boxes
  • sequent calculus
  • link with intuitionistic logic
  • implicit computational complexity
• Denotational semantics
  • relational model
  • coherent model
  • orthogonality