**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 1: life outside a category - categories, functors and natural transformations;
- Lecture 2: life inside a category - isomorphisms, products, duality, universal properties, limits, adjunctions;
- Lecture 3: application to Computer Science - semantics of the simply typed lambda calculus via cartesian closed categories;
- Lecture 4: application to Computer Science - semantics of data types, initial algebras, final coalgebras, nested types.
- Lecture 5 (extra): application to Computer Science - monads.

**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:

- Avoiding unnecessary naming
- Construction versus verification
- Calculational method

Lecture material:

- Slides Lecture 1
- Slides Lecture 2
- Slides Lecture 3
- Slides Lecture 4
- Recounting the Rationals: Twice!
- Exercises in Quantifier Manipulation

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

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.

- Slides Lecture 1 & 2
- Slides Lecture 1 & 2, 4 up
- Slides Lecture 1 & 2, 9 up
- Slides Lecture 3
- Slides Lecture 3, 4 up
- Slides Lecture 3, 9 up

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