Functional Data Structures

Chair for Logic and Verification


Professor Prof. Tobias Nipkow, lectures held by Fabian Huch
Lecture Fri 12:00-14:00
Tutorial Tue 14:00-16:00
Start Lecture 21.04., Tutorial 25.04.
Language English
TUMonline IN2347
Submission System Proving for Fun
Discussion Platform Zulip FDS streams: Announcements (mandatory) and Discussion
Tutorial Organizers Fabian Huch
Exam Wed 09.08.2023, 13:30-15:30, Room 003



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: