Functional Data Structures

Chair for Logic and Verification


Professor Prof. Tobias Nipkow
Lecture (recorded) Friday, 8:30-10:00
Tutorial (remote) Friday, 12:00-14:00
First Lecture 16.4.
Language English
TUMonline IN2347
Submission System Proving for Fun
Tutorial Sessions BigBlueButton
Discussion Platform Zulip FDS streams: Announcements, Discussion, and Off-topic
Solutions and Tutorial Recordings moodle
Tutorial Organizers Fabian Huch



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: