PhD Course - Structural Proof Theory
Organiser(s):
Nicolas Guenot (ngue@itu.dk)
Lectureres:
Nicolas Guenot (ITU) & Taus Brock-Nannestad (INRIA, France)
Date(s) of the course:
Every Wednesday from 5/11/2014 to 17/12/2014
Time:
10:00-12:00
Room:
TBA
Course description:
Structural proof theory, as founded by Gentzen's seminal paper on natural deduction and the sequent calculus, is concerned with the structure of proof objects more than plain provability in a given logic. Through the view of the Curry-Howard correspondence, this means being interested in the structure
of programs, and therefore logic has been a guiding principle in the development of well-behaved models of computation throughout its development. The goal of this course is to present the fundamentals of structural proof theory as well as some of the most important developments that have happened in the last few decades, following the introduction of linear logic. It will emphasize the structural, syntactic approach to formal logic and illustrate the computational significance of each step taken on the side of pure proof theory as well as the influence of research on computational models on the recent development of proof theory.
Program:
5/11: Overview and history of structural proof theory, and relation to the development of the Curry-Howard correspondence
12/11: intuitionistic natural deduction, typed lambda-calculi, correspondence of normalisation with
computation, from simple types to system F
19/11: from natural deduction to the sequent calculus, classical logic and problems with the
computational interpretation of proofs, solutions including lambda-bar and the lambda-mu-calculus
26/11: classical constructivism in linear logic, linear decomposition of classical and intuitionistic
logics, and normalisation as computation in linear logic
3/12:focusing in the sequent calculus, and proof search as computation
10/12: proof-nets for linear logic and related formalisms, and the question of the identity of proofs
in linear, intuitionistic and classical logics
17/12: the deep inference methodology, from the sequent calculus to hypersequents, to the
calculus of structures and open deduction
Reading list:
- M. Sørensen and P. Urzyczyn: Lectures on the Curry-Howard Isomorphism (chapters 3 and 4)
- H. Herbelin: A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure
- J-Y. Girard: Linear Logic
- C. Liang and D. Miller: Focusing and Polarization in Intuitionistic Logic
- D. Hughes and R. van Glabbeek: Proof Nets for Unit-free Multiplicative-additive Linear Logic
- K. Brünnler: Locality for Classical Logic
Prerequisites:
Participants should have a basic knowledge of logic and the lambda calculus
Exam:
Evaluation based on participation and exercises handed in
Credits: 3 ECTS
Amount of hours the student is expected to use on the course:
Participation: 14 hrs.
Preparation : 72 hrs. exercises + paper reading
Website:
Can be found here