Functional Data Structures

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

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.

The syllabus is still evolving. There is likely to be an emphasis on search trees and priority queues.

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: News Lecture and Exercises Homework Important notice Literature

News

Material

Material will be provided via a bitbucket repository, such that you can easily keep up to date.

Lectures will be recorded using the TTT tool. The recordings can be downloaded from the TTT Recordings Website (as soon as they have been processed and uploaded). Last year's recordings: here

Exercises

Provided via the bitbucket repository.

Homework

Homework is the heart and soul of this course and most homework needs to be carried out with Isabelle.

Important notice

Literature

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