Functional Data Structures

Chair for Logic and Verification


Professor Prof. Tobias Nipkow
Lecture Tuesday, 14:00-16:00. stream/recording
Tutorial Friday, 12:00-14:00. stream/recording
First Lecture 26.4.
Language English
TUMonline IN2347
Submission System Proving for Fun
Discussion Platform Zulip FDS streams: Announcements (mandatory) and Discussion
Solutions moodle
Tutorial Organizers Fabian Huch
Exam Fr, 12.08.2022, 8:00 to 10:00 in Room Hörsaal 2, “Interims I” (5620.01.102) (in-person using Isabelle)



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 to prove both functional and complexity properties about them with the theorem prover Isabelle.



Homework is the heart and soul of this course.

Further Literature

This is the canonical reference to functional data structures: