T:+44(0) 115 8232342
F:+44(0) 115 9514254
venanzio.capretta @ nottingham.ac.uk
office: A07
University of Nottingham, 11-15 April 2011
The Midlands Graduate School (MGS) in the Foundations of Computing Science is a collaboration between researchers at the Universities of Birmingham, Leicester, Nottingham and Sheffield. It was established in 1999. The MGS has two main goals: to provide PhD students with a sound basis for research in the mathematical and practical foundations of computing and to give PhD students the opportunity to make contact with established researchers in the field and their peers who are at a similar stage in their research careers.
This year, the MGS is at the University of Nottingham. It will start on 11 April and finish on 15 April.
As in previous years, MGS consists of nine courses, each with five hours of lectures plus exercise sessions. One third of the programme offers introductory (or core) courses which all participants attend. The remainder provides advanced (or specialised) courses from which each participant selects a subset depending upon his or her interests.
| Course Title | Lecturer | Affiliation |
|---|---|---|
| Functional Programming | Henrik Nilsson | Nottingham |
| Category Theory | Thorsten Altenkirch | Nottingham |
| Typed Lambda Calculi | Andrzej Murawski | Leicester |
| Course Title | Lecturer | Affiliation |
|---|---|---|
| Coalgebra | Paul Blain Levy | Birmingham |
| Game Semantics and Applications | Dan Ghica | Birmingham |
| Game Theory, Topology and Proof Theory for Functional Programming | Martín Escardó | Birmingham |
| Process Calculi for Protocol Verification | Eike Ritter | Birmingham |
| Mechanized Theorem Proving | Georg Struth | Sheffield |
In addition to the standard program, Professor Andrew M Pitts from the University of Cambridge will give an invited course on Nominal sets and their applications.
Abstracts and Schedule of Courses
The deadline for registration for MGS 2011 is Friday, 18 March. The registration fee is £400.
This includes accommodation (from Sunday 10 to Friday 15 April), catering for lunches and coffee breaks, and the conference dinner. Accommodation is at the University's Southwell Hall of Residence and includes breakfast.Some student grants may be available, depending on support from funding agencies. Students that successfully apply for a grant will receive a reimbursement for part of the registration fee. To be eligible for application, you must get a letter of support from your supervisor.
To register for MGS 2011, please fill in the following form and send it (preferably by fax or e-mail) to the given address. If you're paying the registration fee by credit card, please use the given form and send it together with the registration. If you want to apply for a student grant, you must provide a letter of support from your supervisor.
Fax: +44(0) 115 9514254
E-mail: liz.clunie@nottingham.ac.uk
For any additional information, contact the local organiser, Venanzio Capretta, at the address vxc@cs.nott.ac.uk.
You can find directions to the School of Computer Science and to your accommodation on the University's How to Find Us web page. There is also a map of Jubilee Campus: The accommodation is at Southwell Hall, you can check in on Sunday 10 April from 1p.m. until midnight; On the morning of the 11th, please come to the Atrium of the Computer Science building for registration and the begginning of MGS. Check-out time on Friday 15 April is at 10a.m., but storage room for luggage will be available for the rest of the day.
Wireless connection. While at the school, you can connect to the internet via the University's guests network (UoN-guest).
| Time | Activity | Room | |||
|---|---|---|---|---|---|
| Monday 11 April | |||||
| 8:00 - 9:00 | Registration | CS Atrium | |||
| 9:00 - 10:00 | Functional Programming | C60 | |||
| 10:00 - 11:00 | Category Theory | C60 | |||
| 11:00 - 11:30 | Coffee Break | CS Atrium | |||
| 11:30 - 12:30 | Nominal Sets | C60 | |||
| 12:30 - 14:00 | Lunch | CS Atrium | |||
| 14:00 - 15:00 | Typed Lambda Calculi | C60 | |||
| 15:00 - 16:00 | Coalgebra | C60 | Process Calculi for Protocol Verification | Amenities B18 | |
| Exercises: Functional Programming | C1 | ||||
| 16:00 - 16:30 | Coffee Break | CS Atrium | |||
| 16:30 - 17:30 | Game Semantics and Applications | C60 | |||
| Mechanized Theorem Proving | Amenities B18 | ||||
| Exercises: Category Theory | C1 | ||||
| 17:30 - 18:30 | Game Theory, Topology and Proof Theory for Functional Programming |
C60 | |||
| Exercises: Typed Lambda Calculi | C1 | ||||
| Tuesday 12 April | |||||
| 9:00 - 10:00 | Functional Programming | C60 | |||
| Exercises: Coalgebra | C1 | ||||
| 10:00 - 11:00 | Category Theory | C60 | |||
| Exercises: Process Calculi | Amenities B18 | ||||
| 11:00 - 11:30 | Coffee Break | CS Atrium | |||
| 11:30 - 12:30 | Nominal Sets | C60 | |||
| 12:30 - 14:00 | Lunch | CS Atrium | |||
| 14:00 - 15:00 | Typed Lambda Calculi | C60 | |||
| Exercises: Mechanized Theorem Proving | Amenities B18 | ||||
| Exercises: Game Theory, Topology and Proof Theory for Functional Programming |
C1 | ||||
| 15:00 - 16:00 | Coalgebra | C60 | Process Calculi for Protocol Verification | Amenities B18 | |
| Exercises: Functional Programming | C1 | ||||
| 16:00 - 16:30 | Coffee Break | CS Atrium | |||
| 16:30 - 17:30 | Game Semantics and Applications | C60 | |||
| Mechanized Theorem Proving | Amenities B18 | ||||
| Exercises: Category Theory | C1 | ||||
| 17:30 - 18:30 | Game Theory, Topology and Proof Theory for Functional Programming |
C60 | |||
| Exercises: Typed Lambda Calculi | C1 | ||||
| Wednesday 13 April | |||||
| 9:00 - 10:00 | Functional Programming | C60 | |||
| Exercises: Coalgebra | C1 | ||||
| 10:00 - 11:00 | Category Theory | C60 | |||
| Exercises: Process Calculi | Amenities B17 | ||||
| Exercises: Nominal Sets | C1 | ||||
| 11:00 - 11:30 | Coffee Break | CS Atrium | |||
| 11:30 - 12:30 | Nominal Sets | C60 | |||
| 12:30 - 14:00 | Lunch | CS Atrium | |||
| 14:00 - 15:00 | Typed Lambda Calculi | C60 | |||
| Exercises: Mechanized Theorem Proving | Amenities B17 | ||||
| Exercises: Game Theory, Topology and Proof Theory for Functional Programming |
C1 | ||||
| 15:00 - 16:00 | Coalgebra | C60 | Process Calculi for Protocol Verification | Amenities B17 | |
| Exercises: Functional Programming | C1 | ||||
| 16:00 - 16:30 | Coffee Break | CS Atrium | |||
| 16:30 - 17:30 | Game Semantics and Applications | C60 | |||
| Mechanized Theorem Proving | Amenities B17 | ||||
| Exercises: Category Theory | C1 | ||||
| 17:30 - 18:30 | Game Theory, Topology and Proof Theory for Functional Programming |
C60 | |||
| Exercises: Typed Lambda Calculi | C1 | ||||
| Thursday 14 April | |||||
| 9:00 - 10:00 | Functional Programming | C60 | |||
| Exercises: Coalgebra | C1 | ||||
| 10:00 - 11:00 | Category Theory | C60 | |||
| Exercises: Process Calculi | Amenities B18 | ||||
| 11:00 - 11:30 | Coffee Break | CS Atrium | |||
| 11:30 - 12:30 | Nominal Sets | C60 | |||
| 12:30 - 14:00 | Lunch | CS Atrium | |||
| 14:00 - 15:00 | Typed Lambda Calculi | C60 | |||
| Exercises: Mechanized Theorem Proving | Amenities B18 | ||||
| Exercises: Game Theory, Topology and Proof Theory for Functional Programming |
C1 | ||||
| 15:00 - 16:00 | Coalgebra | C60 | Process Calculi for Protocol Verification | Amenities B18 | |
| Exercises: Functional Programming | C1 | ||||
| 16:00 - 16:30 | Coffee Break | CS Atrium | |||
| 16:30 - 17:30 | Game Semantics and Applications | C60 | |||
| Mechanized Theorem Proving | Amenities B18 | ||||
| Exercises: Category Theory | C1 | ||||
| 17:30 - 18:30 | Game Theory, Topology and Proof Theory for Functional Programming |
C60 | |||
| Exercises: Typed Lambda Calculi | C1 | ||||
| 20:00 | Dinner | Kayal | |||
| Friday 15 April | |||||
| 9:00 - 10:00 | Functional Programming | C60 | |||
| Exercises: Coalgebra | C1 | ||||
| 10:00 - 11:00 | Category Theory | C60 | |||
| Exercises: Process Calculi | Amenities B18 | ||||
| 11:00 - 11:30 | Coffee Break | CS Atrium | |||
| 11:30 - 12:30 | Typed Lambda Calculi | C60 | |||
| Exercises: Mechanized Theorem Proving | Amenities B18 | ||||
| Exercises: Game Theory, Topology and Proof Theory for Functional Programming |
C1 | ||||
| 12:30 - 14:00 | Lunch | CS Atrium | |||
| 14:00 | School Finishes | ||||
Here is a brief description of the content of each course. Click on the title to get the lecture notes.
This is an introductory taster course introducing some basic concepts of caetgory theory relevant in Computer Science. The course essentially depends on the participants doing exercises and attending exercise sessions. The following topics are covered to some degree:
Monads are a common technique in functional programming, particularly in Haskell, which has direct support for them. I will discuss a new monad, the selection monad, which has applications to game theory (playing games optimally), proof theory (extracting computational information from classical proofs that use the axiom of choice), topology (Tychonoff Theorem), higher-type computation (exhaustive search over infinite sets in finite time). We will also discuss how this is related to the continuation monad, and we will understand the continuation monad from a point of view completely different from the traditional one based on control. The course will be a mix of theory (maths, logic) and application (lots of fun programs in Haskell).
The course will include: basic concepts of game semantics; the fully abstract game model of a procedural concurrent programming language; concrete algorithmic representations of game models and applications to program verification; Geometry of Synthesis, a semantic framework for circuit design; extracting circuit descriptions from game semantics; a survey of open problems in game semantics and applications.
State transition systems are widespread in computer science.
Coalgebra is a more abstract approach to these transition systems.
First we shall see what a coalgebra is, and a number of examples
involving input, output, nondeterminism, divergence and (discrete)
probability. In particular, we look at final coalgebras, which are
used to represent data types such as lazy lists and lazy trees.
We look at various kinds simulation and bisimulation, and see how they
can be brought together using the notion of a relator.
Finally we see that simulation and bisimulation can be characterized
using a final coalgebra, and conversely that we can construct a final
coalgebra by taking an extensional quotient.
This will be an introductory course to the lambda calculus covering classic results regarding its operational and denotational semantics as well as connections with logic.
This is an intermediate-level course on functional programming seeking to
deepen the participants understanding of functional programming and its
possibilities through a series of loosely connected lectures on a few selected
topics. Basic functional programming experience in a modern functional
language featuring a parametrically polymorphic type system, like Haskell or
ML, is assumed. The language used in the course is Haskell.
The exact content will be decided nearer to the time, but covered
topics typically include:
Names and constructs that bind names are ubiquitous in programming languages. Nominal sets provide a mathematical theory of structures involving names that was introduced by the lecturer and Jamie Gabbay about 10 years ago. The theory is based on some simple, but subtle ideas to do with permutations of names and the notion of "finitely supported" mathematical structures which first arose in mathematical logic in the 1930s. The theory has turned out to have some interesting logical and computational properties, with applications to programming language semantics, machine-assisted theorem proving and the design of functional and logical metaprogramming languages. The lectures will introduce the theory of nominal sets and survey some of its applications.
In this lecture course I will present the applied Pi-calculus, a process calculus specifically designed for the verification of security protocols. I will give example of security protocols and security properties and show how both the protocols and the properties can be modelled in the applied Pi-calculus. I will also briefly present ProVerif, which is a tool for automatically verifying security properties specified in the applied Pi-calculus.
Mechanised theorem proving systems are becoming increasingly attractive for mathematicians and computer scientists. They can be surprisingly helpful for developing and analysing mathematical structures and proving deep mathematical theorems. They have been used for various hardware and software verification tasks, e.g., in security protocols, operation systems, static analysis.
Traditionally there have been interactive theorem proving systems (ITP) systems, usually based on higher-order logic, first-order automated theorem proving systems (ATP) systems, as well as special-purpose decision procedures and solvers. But in theorem proving environments such as Isabelle, these tools have been combined in order to benefit from the expressivity of ITP and the proof automation of ATP.
These lectures focus mainly on ATP technology. They introduce the theoretical foundations behind ATP systems, explain some application in mathematical reasoning, discuss some fun examples, and sketch the integration of ATP into the Isabelle theorem proving environment. By attending these lectures, you will learn how ATP systems work, what their potential is and how you could use them for your own research.
In the theory part I will survey some basics from rewriting and universal algebra, including term unification, recursive term orderings and Knuth-Bendix completion. These techniques are equally fundamental for computer algebra, e.g., Groebner bases. I will then present the superposition calculus which underlies most ATP systems, and which combines these techniques with normal form transformations and specific inference rules for first-order equational logic.
In the applications part I will show how ATP systems and counterexample generators lead to a new experimental style of mathematics, an automated game of conjectures and refutations. Examples depend on the interests of the audience and might include semigroups, lattices or relation algebras. I will also show how ATP can be used as a declarative programming tool for solving some logical and combinatorial puzzles.
Finally I will show how Isabelle supports automated theorem proving in theory hierarchies, and offers support for hypothesis learning, symmetries and dualities and theorem instantiation.
The exercise sessions will be organised in an open way, possibly including material from other lectures, to develop and discuss some extended examples.
