Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Mini-courses

Mini-courses

All courses are in FW11 unless stated otherwise.

Term: Lent 2005

Behavioural pseudometrics	Franck van Breugal	1st and 3rd Feb: 10am-11:45
Monads	Nick 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 Ordinals	Thomas 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-Evans	19th Nov: 10am
The simply typed lambda calculus categorically.	Marcelo Fiore	22nd and 26th Nov: 10am-11:45
Concurrency and Pi calculus	Peter Sewell	29th Nov and 3rd Dec

Details

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.

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.

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:

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

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:

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.

Concurrency and Pi calculus

Peter Sewell
29th Nov and 3rd Dec