MGS 2007 Course Descriptions

Operational Semantics
Roy Crole, University of Leicester

Two languages are presented, a simple imperative language with state, and a simple pure (that is, stateless) eager functional language. For each language we present an evaluation (natural) semantics, an abstract machine, and we prove that the machine and evaluation semantics are mutually correct. This forms a nice story for a course of five (rapid) lectures. We do not cover types in great detail (polymorphism and type inference are not covered). Also, we do not cover transition (Plotkin) semantics, nor any form of lazy evaluation for the functional language. The MGS notes are based on previous courses given by the author which do cover these topics, and also denotational semantics.

Lecture slides and related material are available here.

Category Theory
Neil Ghani, University of Nottingham

My course will cover the basics of category theory and then move on to applications in Computer Science:

Lecture notes are available here.

Typed Lambda Calculus
Paul Levy, University of Birmingham

We learn the typed lambda-calculus, a language for describing functions and tuples, with sum, product and function types. We look at denotational semantics, using sets and functions, the substitution lemma and equational theory. We then explore the consequences of adding computational effects such as divergence, with call-by-value and call-by-name evaluation.

Lecture notes are available here.

Dependently Typed Programming
Thorsten Altenkirch, University of Nottingham

We introduce dependently typed programming using the Epigram system. Dependently typed programming generalizes functional programming to a system where we can program, specify and prove exploiting the Curry-Howard-Equivalence. The course will present selected highlights from the Computer Aided Formal Reasoning module which is offered at Nottingham.

Lecture material is available here

Algorithmic Problem Solving
Roland Backhouse, University of Nottingham

This course is about the art of effective reasoning -- i.e. good and bad technique in the solution of problems of an algorithmic nature. Each lecture will consider the solution of one or more simply-stated problems (some of which may already be familiar to participants). We will then consider good and bad technique in their solution. The final lecture will provide an opportunity for participants to discuss the solution of a problem posed (but not solved) in the first lecture. Some of the discussion points are as follows:

Lecture material:

Domain Theory and Denotational Semantics
Martín Escardó, University of Birmingham

This will be based on the book by Thomas Streicher, Domain Theoretic Foundations of Functional Programming, World Scientific, 2006. I'll confine my attention to pages 1-55 of the electronic version. The topics covered will include PCF vs Haskell and functional programming, denotational semantics, operational vs denotational semantics (adequacy), the full abstraction problem, and applications to computation with infinite objects.

Lecture notes are available here.

Stone Duality
Achim Jung, University of Birmingham

Stone duality establishes a connection between logic/lattices and topological spaces. For those who are most familiar with logic, this provides a way to learn about topology; this route has been traced by Steve Vickers in his book Topology via Logic. For those familiar with Domain Theory, it provides a logical description of domain theoretic (type) constructions. The resulting domain logic is very intuitive and immediately seen to be a meaningful program logic. In this course I will present a little bit of the classical theory of these dualities but then present some recent joint work with Drew Moshier which explains even more conspicuously the role that logic has to play. In the last lecture I will explain how domain constructions relate to constructions on logical theories. The course will draw on a number of others from the MGS programme, notably the courses on Category Theory, Semantics, and Topology and Logic.

Advanced Functional Programming
Henrik Nilsson, University of Nottingham

Monads and Arrows are notions with roots in Category Theory that have found important applications as aids for structuring functional programs and libraries. In the Advanced Functional Programming course, we are going to introduce and explore these notions and their relationships, with an emphasis on practical applications like modular interpreters and embedded domain-specific languages.

Concurrency Theory
Colin Stirling, University of Edinburgh

The course will comprise an introduction to process calculus such as CCS, operational semantics in terms of labelled graphs and the notion of bisimulation equivalence. There will also be an introduction to modal and temporal logics with an emphasis on modal logic with fixed points.

Topology and Logic
Steve Vickers, University of Birmingham

The role of topology in computer science has emphasized something that was already known in pure mathematics: that the points of a topological space can be fruitfully handled as the models of a logical theory (often of observations), and that with a suitable geometric logic the topology is already implicit in the theory. My book Topology via Logic explained the approach, but in a context of classical mathematics. In this course I shall explain how it becomes much more significant in constructive mathematics. An elegant package of deals brings together topology, logic, algebra and category theory, and constructive reasoning comes to have an intrinsic continuity.

The course is based on my chapter Locales and Toposes as Spaces for the forthcoming Handbook of Spatial Logics, and a chapter preprint is available here. It also relates to Achim Jung's course on Stone Duality.

Last updated 24 April 2007