CPSC701.04:  CATEGORICAL PROOF THEORY

(Note: website under construction!)

Lecturer: Robin Cockett
Office: ICT 652
Times: Wed. - Fri.  3:30 -  5:00pm
Place:  ICT 638

COURSE DESCRIPTION:

The course will introduce proof theory and its categorical semantics and will be driven by two motivating examples: linear logic and the semantics of partial functions.  From a computer science perspective the former underlies the semantics of concurrency and the latter computability theory.

The course will be structured as a series of seminars and will be based on a series  of reference papers and texts.  Participants are expected to have some degree of mathematical sophistication and/or experience with logic.  Participants will be expected to complete basic exercises on each topic covered as the semester progresses and to produce a final report which picks up on a topic touched during the semmester.

COURSE OUTLINE:

There are two largely independent threads in this course:

(1) The Theory of Partial Maps:

The theory of partial maps underpins the classical theory of computability: an objective of these lectures is to describe how the theory of partial maps connects to the theory of computability through partial combinatory algebras.  The course will develop the theory of partial functions from basics using restriction categories for which the various completeness theorems will be given.  The course will end with a discussion of Turing categories and computability from this perspective.

Here is a rough outline of topics:

• Introduction to restriction categories: the definition and basics, examples and partial map categories, the completeness theorem.
• Cartesian restriction categories: the partial product, partial limits in general, the completeness theorem, separability, term logic.
• Cartesian closed restriction categories:  partial map classification, partial hom-objects, local closedness and separability, partial toposes.
• Join restriction categories: coproducts, extensivity, distributive restriction categories, compatibility and joins, adherence and the completeness theorem.
• Classical restriction categories: Boolean categories and determinism, the classical completion.
• Partial combinatory algebras:  Turing objects and Turing categories, the partial lambda-calculus, computability, the Scott-Koyman's theorem for partial lambda algebras.
Exercises:
1. Exercise sheet 1: restriction category basics.
Reference material:

Notes:

(2) Linear logic and proof theory:

Linear logic was lintroduced by J-Y Girard and is a logic which is resource sensitive: as such the main interest is lies in its proof theory and an objective of the course is to show how this logic connects to the semantics of concurrency.   The course will focus on the multiplicative and additive fragment as this is the fragment which provides a semantics of concurrency (we will also discuss the modalities).

Here is a rough outline of topics:

• The logic: the sequent calculus of cut elimination, polycategories, representability, cut-elimination, the additives, modalities
• The multiplicative proof theory: introduction to circuits, representability and the correctness criteria, thinning links, empire rewiring.
• Categorical semantics: linearly distributive categories, *-autonomous categories
• The additives: \Sigma-\Pi, communication games, softness, channels, term logics.
• Message passing: the logic of mesage passing, actegories and message passing.

Exercises:
1. Basic exercises on \Sigma\Pi (here).
2. Exercises on monoidal categories and linearly distributive categories (here)
1.  Proofs and Types by J-Y Girard: see Paul Taylor's website for an electronic copy (a very useful basic text).
2. Course on linear logic by Robert DiCosmo and Vincent Danos.
3. Robert Seely's web site.
4. Rick Blute's webs  site
5. Phil Scott's webstite.
6. Chu Spaces (Vaughn Pratt's page)
7. Introduction to linear logic by Torben Brauner
8. Programming languages and linear logic:  Phil Wadler's papers on linear logic.

Notes:
• Poly-\Sigma\Pi logic: the annotated logic and an example of a proof (thanks to Sean Nichols!)
• Steven Cheng's cut-elimination proof for \Sigma-\Pi: