
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
(typedirected partial evaluation) and in typechecking 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. Nbealgorithms 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 domaintheoretic denotational semantics of
a simplytyped lambdacalculus 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 MartinLof'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 propositionsastypes idea extends to dependent
type theories. Lecture 3 will describe the standard categorytheoretic
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 lambdacalculus, 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 callbyvalue and callbyname 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 KnuthBendix 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 firstorder 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.
Slides

Henrik Nilsson: Functional Programming
This is an intermediatelevel 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.
Content:
* 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, objectoriented 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 nontechnical introduction to
Coalgebra as a general theory of systems. It aims at explaining
intuitions and will not making use of category theory. Lectures 24
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 24 will be: Coalgebras, Behavioural
Equivalence/Bisimulation,Final Coalgebras/Final Coalgebra Sequence. I
will finish with an outlook on current research areas connected to Coalgebra.