Functional Data Structures

Overview

Organization

• announcements will be made in Zulip (announcements stream).
• you will get access the moodle course once registered in TUMonline
• if you are not yet enrolled (or have any other question regarding the organization of the course), write to the tutorial organizers
• to follow the tutorial, do listen to the preceding lecture beforehand
• both the lecture and tutorial will take place in-person. Additionally, they will be recorded/streamed. However, interaction during the live stream will not be possible, hence we strongly recommend attending on-site.
• Exercises and installation instructions
• The exam is open-book, i.e., all material from the lecture may be used, as well as your own notes. Downloading the internet is not allowed, as well as using the internet during the exam for anything other than submitting your solution.

Aims

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.

Prerequisites

• 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

Homework is the heart and soul of this course.

• Solved homework should be uploaded to the submission system, according to the instructions on the first exercise sheet. Make sure that your submission gets a “Passed” status in the system. We will not grade it otherwise! If you have any problems uploading, or if the submission seems to be rejected for reasons you cannot understand, please contact the tutor.
• The latest submission date is given on each exercise sheet. Late submissions will not be graded! If you have a good excuse (such as being very sick), you should contact the tutors before the deadline.
• You can upload multiple times; the last upload before the deadline is the one that will be graded.
• If you cannot finish a proof, extract any lemmas you need for it and assume them by using sorry.
• 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.
• Important: all homework is graded and contributes 50% towards the final grade, though you need to pass the final exam.

Further Literature

This is the canonical reference to functional data structures:

• Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999.