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
1st and 3rd June at 10am In FW09 on the 3rd of June.
Abstract. Some time ago I wrote a paper on a rather unexpected
relationship between continuations and classical logic.
I will present the basic results of this paper, and then attempt
to reinterpret those results in a way that may make more sense.
20th, 22nd, and 24th June at 10am
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
you can find
the slides for the course. The fourth slide lists some useful papers.
Franck van Breugal
1st and 3rd Feb: 10am-11:45In FW09 on 3rd Feb
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.
17th and 22nd Feb: 11am-12:30
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
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.
15th, 17th, 21st and 23rd Mar: 10am-11:45
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
For more details see: http://www.cl.cam.ac.uk/~jeh1004/compsci/lectures/ecc.html
10:00-12:00, Tue 15 March: Elliptic Curve Cryptography
This lecture provides a mathematical introduction to elliptic curves
and their applications in cryptography.
10:00-12: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:00-12:00, Mon 21 March and
10:00-12: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.
1st and 5th Nov: 10am-11:45 In FW09
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.
Nov 8th and 12th: 10am - 11:45
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.
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
omega-cppos and strict continuous functions.
Minimal invariant solutions and free bialgebras.
The limit-colimit construction.
- 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
17th Nov: 10am-11:45
Additional lecture 24th Nov: 10-11am
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.)
19th Nov: 10am
22nd and 26th Nov: 10am-11:45
- 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.
- R.Crole. Categories for types. CUP, 1995.
- J.Lambek and P.Scott. Introduction to higher order categorical logic.
- M.Fiore. Semantic analysis or normalisation by evaluation for typed
lambda calculus. PPDP, 2002.
- D.Scott. Relating theories of the lambda calculus. AP, 1980.
29th Nov and 3rd Dec