**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.

(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:

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:

Notes:

- Basic exercises on \Sigma\Pi (here).
- Exercises on monoidal categories and linearly distributive
categories (here)

- 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: