INF image

Venanzio Capretta
School of Computer Science
University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB, UK

T: +44(0) 115 9514251
F: +44(0) 115 9514254

Although computers have a finite memory and cannot store an infinite amount of information, Functional Programming and Type Theory allow us to represent infinite mathematical objects. These are represented as processes that generate part of the structure at every step. The mathematical/categorical formulation for these processes is the notion of coalgebra.

The first part of the course is an introduction to coalgebras with important examples like streams (infinite sequences) and non-well-founded trees. The most powerful proof method for infinite data structures is the Coinduction Principle, which allows us to prove the equality of two objects by a bisimulation, itself an infinite process that generates the equality by successive stages.

We will study methods to construct sound infinite objects, to solve recursive equations on them and to prove their properties. Examples will be given using functional programming in Haskell and formal reasoning in Coq. In Type Theory we can define coinductively not just single types, but families of types, predicates and relations. This leads to a proof technique in which the statement to be proved can be used recursively as long as it satisfies a guardedness conditions. It amounts to constructing a proof with an infinite number of logical steps.

We can combine coinduction with induction in several ways to define types with a complex internal structure. One example is the definition of all continuous functions between streams. A further generalization consists in defining a coinductive type simultaneously with a recursive function on it, in the style of induction-recursion. This leads to a very general notion of Wander types, that can be instantiated to many of the most common type-theoretic constructions.

Outline of lectures

In this section you will find, after each lecture, a list of topics that were taught and references to the chapters of the textbook.

DateTopicsLecture Material
1. Sun 9 Apr 2017 Introduction to Infinite Types
Streams and Non-well-founded Trees
Productivity and Guardedness
Outline of Lecture 1
Chapter 8
of The Construction of Infinity
1E. Mon 10 Apr 2017 Exercise Class 1 Haskell Code
2. Mon 10 Apr 2017 (Final) Coalgebras
Bisimulation and CoInduction
Outline of Lecture 2
Coalgebras in functional programming
and type theory
2E. Tue 11 Apr 2017 Exercise Class 2 Coq Code
3. Tue 11 Apr 2017 Monadic Stream Functions
The Continuity Principle
Outline of Lecture 3
The Continuity of
Monadic Stream Functions

with Jon Fowler
3E. Wed 13 Apr 2017 Exercise Class 3 Haskell Code
4. Wed 12 Apr 2017 CoInductive Reasoning
Common Knowledge
The Coinductive Formulation
of Common Knowledge

with Colm Baston
4E. Thu 13 Apr 2017 Exercise Class 4 Coq Code
A. from MGS 2013 Strategy Trees
Function Tabulation
Lecture A
B. from MGS 2013 Simultaneous (Co)Induction / Recursion
Wander Types
Lecture B
Wander Types