Theory mini-courses
All courses are in FW11 unless stated otherwise. Previous courses can be found here.
If you would like to volunteer a course, please contact Matthew Parkinson.

Term: Easter 2005

A look at continuations and logic. Tim Griffin1st and 3rd June at 10am
Mobile processes and bigraphsRobin Milner 20th, 22nd, and 24th June at 10am

Term: Lent 2005

Behavioural pseudometricsFranck van Breugal 1st and 3rd Feb: 10am-11:45
MonadsNick Benton 17th and 22nd Feb: 11am-12:30
Elliptic Curve Cryptography: A case study in formalization using a higher order logic theorem prover Joe Hurd 15th, 17th, 21st and 23rd Mar: 10am-11:45

Term: Michaelmas 2004

Minicourse on OrdinalsThomas Forster 1st and 5th Nov: 10am-11:45
How to solve recursive domain equations. Andrew Pitts Nov 8th and 12th: 10am - 11:45
Domain theory for concurrency Glynn Winskel 17th Nov: 10am-11:45
Additional lecture 24th Nov: 10-11am
Category theory for dummies (Introduction for Marcelo's course) Lucy Saunders-Evans19th Nov: 10am
The simply typed lambda calculus categorically. Marcelo Fiore 22nd and 26th Nov: 10am-11:45
Concurrency and Pi calculusPeter Sewell29th Nov and 3rd Dec

Details

Easter 2005

A look at continuations and logic.

Tim Griffin
1st and 3rd June at 10am In FW09 on the 3rd of June.
Details:
Abstract. Some time ago I wrote a paper on a rather unexpected relationship between continuations and classical logic. See http://citeseer.ist.psu.edu/griffin90formulaeastypes.html. I will present the basic results of this paper, and then attempt to reinterpret those results in a way that may make more sense.

Mobile processes and bigraphs

Robin Milner
20th, 22nd, and 24th June at 10am
Details:
Bigraphs are an algebraic-cum-graphical model for mobile processes that reconfigure their placing and linking. The prefix `bi' connotes that these two structures, placing and linking, are orthogonal: `where you are doesn't affect who you may talk to'. They aim to be useful for pervasive computing; I can illustrate this briefly with behaviour in a sentient environment.
The model is mildly category theoretic, but most of the work can be (and will be!) seen graphically. There is also an algebraic presentation of bigraphs that lends itself to animation as a programming language. Bigraphs subsume CCS, Petri nets, pi calculus, ambient calculus and lambda calculus. Of course, if you only need one of these you would not use bigraphs; but applications tend to want more than one, and a coordinating model can also be useful to tease out ideas that are in common.
In the examples, I shall use link graphs (half of bigraphs) to model bisimilarity in Petri nets, then pure bigraphs to do the same for CCS. This leads finally to binding bigraphs, where --- as time permits --- I sall treat lambda calculus with explicit substitutions and conjecture a generalsiation of ther Church Rosser theorem (confluence).
At http://www.cl.cam.ac.uk/~rm135/bigraphs-tutorial.pdf you can find the slides for the course. The fourth slide lists some useful papers.

Lent 2005

Behavioural pseudometrics

Franck van Breugal
1st and 3rd Feb: 10am-11:45In FW09 on 3rd Feb
Details:
To model concurrent systems in which quantitative data (like probabilities, time, costs or rewards) plays a crucial role, extensions of labelled transition systems have been put forward. Notions of behavioural equivalence like bisimilarity have been adapted to this setting. However, such discrete Boolean-valued notions (states are either behaviourally equivalent or they are not) sit uneasily with models featuring quantitative data. For example, consider probabilities. If some of the probabilities change a little bit --the probabilities are often obtained experimentally and, hence, are usually approximations-- states that used to be behaviourally equivalent may not be anymore or vice versa. In conclusion, behavioural equivalences like probabilistic bisimilarity are not robust.
To address this problem, pseudometrics that assign a distance, a real number between 0 and 1, to each pair of states of a system have been proposed. Such a pseudometric yields a smooth and quantitative notion of behavioural equivalence. The distance between states is used to express the similarity of their behaviour. The smaller the distance, the more alike the systems behave. In particular, the distance between systems is 0 if they are behaviourally indistinguishable.

Monads

Nick Benton
17th and 22nd Feb: 11am-12:30
Details:
A tension in language design has been between simple semantics on the one hand, and rich possibilities for side-effects, exception handling and so on on the other. The introduction of monads has made a large step towards reconciling these alternatives. First proposed by Moggi as a way of structuring semantic descriptions, they were adopted by Wadler to structure Haskell programs.
Monads have been used to solve long-standing problems such as adding pointers and assignment, inter-language working, and exception handling to Haskell, without compromising its purely functional semantics.
The course introduces monads, effects, and exemplifies their applications in programming and in compilation.
The course presents typed metalanguages for monads and related categorical notions, and then describes how they can be further refined by introducing effects.

Elliptic Curve Cryptography: A case study in formalization using a higher order logic theorem prover

Joe Hurd
15th, 17th, 21st and 23rd Mar: 10am-11:45
Details:
Formalizing a mathematical theory using a theorem prover is a necessary first step to proving the correctness of programs that refer to that theory in their specification. In this course I will show how modern higher order logic theorem provers help (and occasionally hinder) such formalizations. The case study for the course will be a formalization of (the foundations of) elliptic curve cryptography using the HOL4 theorem prover, and part of the course will be an introduction to the mathematics of public key cryptography and elliptic curves.
For more details see: http://www.cl.cam.ac.uk/~jeh1004/compsci/lectures/ecc.html

Michaelmas 2004

Minicourse on Ordinals

Thomas Forster
1st and 5th Nov: 10am-11:45 In FW09
Details:
Ordinals are transfinite analogues of natural numbers, and are of great importance in CS because they give a precise and illuminating way of describing the complexity of various recursions.

How to solve recursive domain equations.

Andrew Pitts
Nov 8th and 12th: 10am - 11:45
Details:
My aim is to give the up-to-date (post-Freydian) view on the solution of recursive domain equations. I will try to keep things as concrete as possible, by taking "domain" to mean "omega-chain complete partially ordered set with a least element"; familiarity with the first half of the Part II course on Denotational Semantics will be assumed. However, a certain amount of category theory is essential: some familiarity with the notions of "category" (and the opposite of a category), "functor", "natural transformation", "limit" and "colimit" will be assumed, but not much more.
Outline: Reference:

Domain theory for concurrency

Glynn Winskel
17th Nov: 10am-11:45
Additional lecture 24th Nov: 10-11am
Details:
Abstract: I'll present a simple domain theory for concurrency. Although a domain theory for nondeterministic processes it also forms a model of linear logic in which there are comonads interpreting variants of the linear logic exponential. The model highlights the role of linearity in concurrent computation. Two choices of comonad yield two expressive metalanguages for higher-order processes, both arising from canonical constructions in the model. Their denotational semantics are fully abstract with respect to contextual equivalence. One language derives from an exponential of linear logic; it supports a straightforward operational semantics with simple proofs of soundness and adequacy. The other choice of comonad yields a model of affine-linear logic, and a process language with a tensor operation which can be understood as a parallel composition of independent processes. I'll conclude with a discussion of a broader programme of research, towards a comprehensive domain theory for concurrency. I hope these talks will motivate, give background and references to domain theory, category theory, linear logic, ..., the subjects of future mini-courses. (This is based on joint work with Mikkel Nygaard.)

Category theory for dummies (Introduction for Marcelo's course)

Lucy Saunders-Evans
19th Nov: 10am


The simply typed lambda calculus categorically.

Marcelo Fiore
22nd and 26th Nov: 10am-11:45
Details:
Topics: References:

Concurrency and Pi calculus

Peter Sewell
29th Nov and 3rd Dec