University of Leicester


Midlands Graduate School

Course Descriptions

  • Thorsten Altenkirch: Categories for the Lazy Functional Programmer

    Course material

  • Peter Dybjer: Normalization by Evaluation

    Normalization by evaluation (nbe) is a new method for writing normalization algorithms. The idea is to first build a data structure which represents a model of the language in question. Then terms are interpreted in this model, and finally the normal forms are extracted from the semantic values. The method has both practical and theoretical interest. It has been used for program simplification (type-directed partial evaluation) and in type-checking algorithms for proof assistants based on type theory. Ideas from several fields in theoretical computer science are useful for analyzing the method, such as constructive type theory and program extraction, category theory, and domain theory. These lectures will give an introduction to the technique and discuss some of these connections. Nbe-algorithms can often be nicely expressed in programming languages with dependent types. For this purpose we shall use Agda, a new dependently typed functional language developed in Gothenburg. We shall show how to use this language both for programs and for proofs of correctness of nbe- algorithms.

    Notes, Exercises and Agda Files

    Combinators.agda Lam*.agda Nbe.agda NbeSound.agda Power.agda Sets.agda Laws.agda NbeComplete.agda Pentagon.agda Sem.agda Exp.agda TyTm.agda Eta.agda

  • Martin Escardo: Semantics

    We'll study operational and domain-theoretic denotational semantics of a simply-typed lambda-calculus with general recursion and base types for natural numbers and booleans, and with a type constructor for (finite and infinite) streams. This corresponds to a subset of Haskell, and hence attendance to the Haskell course will be helpful for this course, although formally it is not a prerequisite. We'll apply domain theory to discover programs that one would hardly come up with without topological methods associated to domain theory, which we'll also develop to some extent.

  • Nicola Gambino: Dependent Type Theory

    The lecture course will consist of four lectures. Lecture 1 will present Martin-Lof's dependent type theories, so as to fix notation and terminology for the subsequent lectures. Lecture 2 will present some fundamental facts about dependent type theories. For example, we will explain how the propositions-as-types idea extends to dependent type theories. Lecture 3 will describe the standard category-theoretic semantics of dependent type theories in locally cartesian closed categories, explaining its limitations. Lecture 4 will be an introduction to some of the ongoing research on relating dependent type theories and homotopical algebra.

    Summary notes

  • Paul Levy: The Lambda Calculus

    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.

  • Georg Struth: Automated Theorem Proving

    Automated theorem proving systems (ATP systems) are becoming increasingly attractive for mathematicians and computer scientists. They can be surprisingly helpful for developing and analysing mathematical structures. They have been used, e.g., for protocol analysis and integrated into static analysis tools. They can be turned into effective decision procedures for applicative logics in knowledge representation or constraint solving.

    These lectures introduce the theoretical foundations behind ATP systems, explain some application in mathematical reasoning and discuss some fun examples. 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., Gr\"obner 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 show how the superposition calculus specialises to efficient decision procedures for some classes of formulas. I will also show how ATP can be used as a declarative programming tool for solving some logical and combinatorial puzzles.

    The exercise sessions will be organised in an open way, possibly including material from other lectures, to develop and discuss some extended examples.


  • Henrik Nilsson: Functional Programming

    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.


    * Lazy functional programming techniques

    * Purely functional data structures

    * Monads and monad transformers

    * Concurrency

    The course is supported by exercise sessions.

    Course material

  • Uday Reddy: Separation Logic

    Separation Logic is a reasoning system for dynamic data structures, more generally, dynamic resources, invented by Reynolds, O'Hearn and Pym at the turn of the century. The subject has seen rapid development over the last decade with significant progress made in treating various programming features including systems programs, object-oriented programs and concurrent programs. There is also active research in developing automated verification systems and static analysis systems. This course will cover the basic theory of the subject, leading up to the logic RGSep developed by Vafeiadis for treating concurrency.

    Reference material: John Reynolds's minicourse
  • Alexander Kurz: Coalgebra

    The first lecture will give a general non-technical introduction to Coalgebra as a general theory of systems. It aims at explaining intuitions and will not making use of category theory. Lectures 2-4 will then explain some of the theory of coalgebra in more detail. Basic knowledge of category theory would be helpful here (limits, colimits, adjoints), but I will try to keep technicalities to a minimum. The topics of lectures 2-4 will be: Coalgebras, Behavioural Equivalence/Bisimulation,Final Coalgebras/Final Coalgebra Sequence. I will finish with an outlook on current research areas connected to Coalgebra.

Author: Roy Crole.
University of Leicester February 2009. Last modified: 7th April 2009, 21:21:18.
Informatics Web Maintainer. This document has been approved by the Head of Department.