Title: Proof-theory: from classical to linear logic
Lecturer: Gabriele Pulcini
Period: april 2014 (20 hrs, 4 CFR)
Abstract In the first part of the course, the three main deductive systems for classical and intuitionistic logics will be provided: Hilbert calculi, natural deduction systems and Gentzen-style sequent calculi. In particular, we will dwell on Gentzen systems so as to prove both the cut-elimination and the subformula properties. Moreover, we will expound the Curry-Howard correspondence linking intuitionistic proofs to formal computations.
The second part will be entirely devoted to linear logic (LL). After informally discussing – from a strictly proof-theoretical point of view – both the notions of substructurality and resource awareness, we will introduce the cluster of linear connectives and their respective syntax. As far as the multiplicative fragment of LL is concerned, we will also provide the parallel syntax in terms of proof-nets.
- an introduction to proof theory
- natural deduction (classic and intuitionistic)
- sequent calculus (classic and intuitionistic)
- cut-elimination and the subformula property
- lambda-calculus and the Curry-Howard correspondence
- linear logic (sequent calculus)
- multiplicative proof-nets
- Lesson 1. Wed 23.4, h. 14.15-16.15 Aula F
- Lesson 2. Thu 24.4, h. 14.15-16.15 Aula F
- Lesson 3. Tue 29.4, h. 14.15-16.15 Aula B
- Lesson 4. Wed 30.4, h. 14.15-16.15 Aula F
- Lesson 5. Tue 13.5, h. 14.15-16.15 Aula F
- Lesson 6. Wed 14.5, h. 14.15-16.15 Aula F
- Lesson 7. Thu 29.5, h. 14.15-16.15 Aula F
- Lesson 8. Thu 5.6, h. 14.15-16.15 Aula F
- Lesson 9. Fri 6.6, h. 14.15-16.15 Aula F
- D. van Dalen. Intuitionistic Logic. In (Ed. L. Goble) Philosophical Logic, Blackwell, Oxford. 224-257.
- V. Danos & R. Di Cosmo. Linear Logic Primer. Draft
- J.-Y. Girard. Proofs and Types. CUP
- J.-Y. Girard. Proof Theory and Logical Complexity. Bibliopolis
- J.-Y. Girard. Linear Logic, its syntax and semantics. Advances in Linear Logic, eds Girard, Lafont, Regnier, London Mathematical Society LNS 222, CUP 1995.