-
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.
Slides
-
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.
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, 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.