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
Term: Lent 2005
Term: Michaelmas 2004
Details
Easter 2005
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.
Robin Milner
20th, 22nd, and 24th June at 10am
Details:
Bigraphs are an algebraiccumgraphical 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/bigraphstutorial.pdf you can find
the slides for the course. The fourth slide lists some useful papers.
Lent 2005
Franck van Breugal
1st and 3rd Feb: 10am11:45
In 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 Booleanvalued 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.
Nick Benton
17th and 22nd Feb: 11am12:30
Details:
A tension in language design has been between simple semantics on the
one hand, and rich possibilities for sideeffects, 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 longstanding problems such as adding
pointers and assignment, interlanguage 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.
Joe Hurd
15th, 17th, 21st and 23rd Mar: 10am11: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

10:0012:00, Tue 15 March: Elliptic Curve Cryptography
This lecture provides a mathematical introduction to elliptic curves
and their applications in cryptography.

10:0012:00, Thu 17 March: Introduction to HOL
This lecture is a tutorial introduction to the HOL4 theorem prover,
aimed at getting a newbie up and proving as quickly as possible.

10:0012:00, Mon 21 March and
10:0012:00, Wed 23 March: Formalized Elliptic Curves
The details of how the mathematics of Elliptic Curves Cryptography is
formalized in HOL, as a medium scale case study that will be used as a
golden reference for verifying programs.
Michaelmas 2004
Thomas Forster
1st and 5th Nov: 10am11: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.
Andrew Pitts
Nov 8th and 12th: 10am  11:45
Details:
My aim is to give the uptodate (postFreydian) view on the solution
of recursive domain equations. I will try to keep things as concrete
as possible, by taking "domain" to mean "omegachain 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:

Why do we need to solve domain equations and why is it hard to do so?

Locally continuous functors of mixed variance on the category of
omegacppos and strict continuous functions.

Minimal invariant solutions and free bialgebras.

The limitcolimit construction.

Applications (sketchily).
Reference:
 S. Abramsky and A. Jung, Domain Theory.
 Chapter 1 of S. Abramsky and
D. M. Gabbay and T. S. E. Maibaum (eds), Handbook of Logic in
Computer Science, Volume 3. Semantic Structures (Oxford University
Press, 1994).
Glynn Winskel
17th Nov: 10am11:45
Additional lecture 24th Nov: 1011am
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
higherorder 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
affinelinear 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 minicourses.
(This is based on joint work with Mikkel Nygaard.)
Lucy SaundersEvans
19th Nov: 10am
Marcelo Fiore
22nd and 26th Nov: 10am11:45
Details:
Topics:
 Type theory: syntax and equational theory.
 Categorical models: cartesian closed categories,
soundness and completeness.
 The initial algebra approach: syntax and semantics.
 Lambda definability and normalisation by evaluation.
References:
 R.Crole. Categories for types. CUP, 1995.
 J.Lambek and P.Scott. Introduction to higher order categorical logic.
CUP, 1986.
 M.Fiore. Semantic analysis or normalisation by evaluation for typed
lambda calculus. PPDP, 2002.
 D.Scott. Relating theories of the lambda calculus. AP, 1980.
Peter Sewell
29th Nov and 3rd Dec