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
here.
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
–
12 noon | FW26 |
| An introduction to Isabelle | Larry Paulson | November 21st, 23rd, 25th, 28th, 29th and December 2nd,
12 noon
–
1pm | FW26 (21st, 25th, 28th, 29th), FW11 (23rd, 2nd) |
| The nominal datatype package in Isabelle | Christian Urban | December 5th, 7th, 8th,
10 am
–
11am | FW11 (5th, 8th), FW26 (7th) |
Term: Lent 2006
Term: Easter 2006
Details
Michaelmas 2005
Nominal syntax and semantics
(top)
Andrew Pitts
October 10th, 12th and 14th, 10 am
–
12 noon.
Room
FW26
(
map).
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
http://www.cl.cam.ac.uk/users/amp12/talks/appsem2005/.
An introduction to Isabelle
(top)
Larry Paulson
November 21st, 23rd, 25th, 28th,
29th and December 2nd,
12 noon
–
1pm.
Room
FW26 (21st, 25th, 28th, 29th), FW11 (23rd, 2nd)
(
map).
Course materials are found at
http://www.cl.cam.ac.uk/users/lcp/Course/.
This course is an introduction to theorem proving with the
Isabelle/HOL system. It is largely based on the book
Isabelle/HOL
— A
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.
- Sets.
The nominal datatype package in Isabelle
(top)
Christian Urban
December 5th, 7th, 8th,
10 am
–
11am.
Room
FW11 (5th, 8th), FW26 (7th)
(
map).
Slides from lecture one are at
http://www.cl.cam.ac.uk/users/ss368/minicourses/christian1.pdf.
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.
Lent 2006
Formal Verification Techniques
(top)
Hasan Amjad
Monday February 20th, Wed 22nd, Fri 24th, Mon 27th;
Wednesday March 1st, Fri 3rd;
10 am
–
11am.
Room
FW11
(
map).
Course materials are at
http://www.cl.cam.ac.uk/users/ha227/node6.html.
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
(top)
Matthew Parkinson
Tuesday 28th Feb, Thursday 2nd March;
10 am
–
12 noon.
Room
FW26
(
map).
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
- concurrency;
- modularity; and
- decidability.
Easter 2006
Protecting Alice from Malice:
Protocols, Process Calculi, Proved Programs
(top)
Andrew Gordon
Tuesday 16 May and Thursday 18 May, 10 am
–
12 noon.
Room
FW26
(
map).
Slides, and bibliographic notes,
are available
here.
This is a preview of a course this summer at the
International Summer
School Marktoberdorf.
Distributed Programming Languages
(top)
Peter Sewell
Times TBA.
Details will follow.
