Functional Data Structures

Prof. Tobias Nipkow, Dr. Mohammad Abdulaziz, Summer semester 2020

The course introduces students to the design and analysis of data structures for functional programming languages. It assumes that the students are familiar with functional programming and with running time analysis of algorithms. The course covers a range of functional data structures with an emphasis on their precise analysis. Proofs of both functional correctness and complexity will be a core part of the course. Proofs are carried out with the help of a computer-based proof assistant Isabelle. An introduction to Isabelle is part of the course.

There is an emphasis on search trees and priority queues, but the syllabus is still evolving.

At the end of the course students should be familiar with a number of efficient functional data structures and algorithms and should be able able to prove both functional and complexity properties about them with the theorem prover Isabelle.

On this page: Important notices News Written Material Lectures Homework Literature

Important notices

  • You must be familiar with some functional programming language like Haskell, Objective Caml, Standard ML or F# (e.g. Functional Programming and Verification (IN0003)).
  • You must have taken a first course on data structures and algorithms (e.g. Fundamentals of Algorithms and Data Structures (IN0007)).
  • You must have taken some basic course in discrete mathematics where you learned about sets, relations and proof principles like induction (e.g. Discrete Structures).
  • You need not be familiar with formal logic but you must be motivated to learn how to write precise and detailed mathematical proofs that are checked for correctness by a machine, the theorem prover Isabelle.
Homework, exam, grading:
Throughout the course there will be homework assignments. They will involve the use of Isabelle and will be graded. At the end of the course there will be a written or oral examination, depending on the number of students. The final grade will combine the grades from the examination (60%) and the homework (40%).
Discussing ideas and problems with others is encouraged. When working on homework problems, however, you need to solve and write up the actual solutions alone. If you misuse the opportunity for collaboration, we will consider this as cheating.
Plagiarizing somebody else's homework results in failing the course immediately. This applies for both parties, that is, the one who plagiarized and the one who provided his/her solution.
All lectures are in English.
Please install Isabelle 2020 on your computer. You will need Isabelle for (almost) everything, in particular tutorials and homework.


Written Material

All written material (lectures notes, slides, demo material, exercises, homework, ...) will be provided via a github repository, such that you can easily keep up to date.


Until we can all meet safely in the classroom again, all lectures are will be replaced by video recordings of the same. We will use a mixture of TTT recordings from previous years (2018, 2019) and new recordings. For each Friday (when the lecture would take place) we list which recordings to watch and what to read up to that date:



Homework is the heart and soul of this course. It is provided in the repository and needs to be carried out with Isabelle.


There is currently no book that covers the material of the course. However, this is the canonical reference to functional data structures: