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:

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:


Exercises:
  1. Basic exercises on \Sigma\Pi (here).
  2. Exercises on monoidal categories and linearly distributive categories (here)
Reference material and links:
  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: