This is an archive of courses from 2005-2006. Please click here for courses after 2006.
Courses for 2004-2005 are found
here; for courses 2000-2004 look
If you would like to volunteer a course, please contact Sam Staton.
Term: Michaelmas 2005
|Nominal syntax and semantics||Andrew Pitts||October 10th, 12th and 14th, 10 am
|An introduction to Isabelle||Larry Paulson||November 21st, 23rd, 25th, 28th, 29th and December 2nd,
1pm||FW26 (21st, 25th, 28th, 29th), FW11 (23rd, 2nd)
|The nominal datatype package in Isabelle||Christian Urban||December 5th, 7th, 8th,
11am||FW11 (5th, 8th), FW26 (7th)
Term: Lent 2006
Term: Easter 2006
Nominal syntax and semantics
October 10th, 12th and 14th, 10 am
Formal languages involving names and constructs that bind names abound in computer science. Much effort has been expended to find mathematical theories of "syntax modulo renaming bound names" that have good logical and computational properties, but are also easy to use. These lectures introduce the theory and applications of "nominal sets", a new mathematical model of names and binding based on simple, but subtle ideas to do with permutations of names that first arose in mathematical logic in the 1930s. At the heart of the approach is the notion of "finitely supported" mathematical objects. The lectures will explain the idea in as concrete a way as possible and will discuss its consequences for programming language semantics and for the design of functional and logical metaprogramming languages.
This course will be based on lectures given at the APPSEM Summer School.
Notes, slides and exercises can be found at
An introduction to Isabelle
November 21st, 23rd, 25th, 28th, 29th
and December 2nd,
Room FW26 (21st, 25th, 28th, 29th), FW11 (23rd, 2nd)
Course materials are found at
This course is an introduction to theorem proving with the
Isabelle/HOL system. It is largely based on the book
Proof Assistant for Higher-Order Logic
and covers the most important
definition mechanisms and proof methods.
The course is aimed at students who are seriously interested in
becoming acquainted with computer-assisted theorem proving. It
combines a practical how-to approach with the necessary logical
background material. At the end of the course students are able to
define and reason about functional programs, logical and set-theoretic
formulae, and simple mathematical models of discrete systems (for
example in a set-theoretic style). No prior background in theorem
proving is required, but familiarity with and a basic understanding of
logical and mathematical notation and some minimal exposure to
functional programming is assumed.
The course is divided into 6 one-hour lectures.
- Basic notation. Recursion and induction on lists.
- Datatypes and primitive recursive functions.
- Simplification. Induction heuristics.
- Propositional logic.
- Predicate logic.
The nominal datatype package in Isabelle
December 5th, 7th, 8th,
Room FW11 (5th, 8th), FW26 (7th)
Slides from lecture one are at
This course will explain the theory and applications of the
nominal datatype package. This datatype package provides an
infrastructure for reasoning about languages involving binders.
I will illustrate how informal proofs about the lambda-calculus
can be formalised with ease in Isabelle/HOL using the nominal
datatype package. I will further explain how strong induction
principles can be derived that have Barendregt's variable
convention already built in.
Formal Verification Techniques
Monday February 20th, Wed 22nd, Fri 24th, Mon 27th;
Wednesday March 1st, Fri 3rd;
Course materials are at
Formal verification constructs mathematical proofs about the behaviour of computer hardware and software. As a heavy user of mathematical logic, it has strong connections with theoretical computer science.
This mini-course will present a survey of current formal verification methods. Enough detail will be given to establish clear connections with the underlying theory, and to give some idea of the problems facing the field.
Pre-requisities: The mini-course aims to be self contained. Some familiarity with logic will make the going easier.
The course is divided into 6 one-hour lectures.
- Introduction. Theorem proving. Propositional Logic. First-order logic.
- Arithmetic. Higher-order logic.
- Model Checking. Computation Tree Logic. OBDDs. Symbolic model checking.
- Linear Time Logic. Fairness. The propositional mu-calculus.
- SAT-solvers. SAT-modulo-theory solvers.
- Predicate abstraction. Automatic abstraction refinement.
Introduction to Separation Logic
Tuesday 28th Feb, Thursday 2nd March;
Separation logic is an extension to Hoare logic that allows reasoning about datastructures involving
pointers. The first part will cover:
- the historical background;
- the definition of the logic; and
- provide example verification of some sequential programs.
The second will present more advanced issues of the logic including
- modularity; and
Protecting Alice from Malice:
Protocols, Process Calculi, Proved Programs
Tuesday 16 May and Thursday 18 May, 10 am
Slides, and bibliographic notes,
are available here
This is a preview of a course this summer at the
Distributed Programming Languages
Details will follow.