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:
- 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:
- Basic exercises on \Sigma\Pi (here).
- Exercises on monoidal categories and linearly distributive
categories (here)
Reference material
and links:
- Proofs and Types
by J-Y Girard: see Paul
Taylor's website for an electronic copy (a very useful basic text).
- Course on linear logic by Robert
DiCosmo and Vincent Danos.
- Robert Seely's
web site.
- Rick Blute's webs
site
- Phil Scott's
webstite.
- Chu Spaces (Vaughn Pratt's
page)
- Introduction to linear logic by Torben
Brauner
- 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: