Functional Data Structures

Dr. Peter Lammich, Prof. Tobias Nipkow, Summer semester 2017

• Module: IN2347 SS17
• Lectures: 2 lecture hours per week, Fri 8:30-10:00 MI Hörsaal 3
• Tutorials: 2 lecture hours per week, Fri, 12:15-13:45 MI Hörsaal 2
• Start of lectures: first week (April 28). Start of tutorials: first week (April 28)
• Tutors: Peter Lammich

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.

This course is brand new and 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

• The written exam
  • You will be allowed to use 1 handwritten or printed A4 sheet of paper, but nothing else.
  • A few questions may be Isabelle-specific, but the majority will deal with programs and proofs.
  • Proofs must be detailed and readable but need not conform exactly to the Isabelle syntax. Major proof steps, especially inductions, need to be stated explicitly. Minor proof steps (corresponding to by simp, by blast etc) need not be justified if you think they are obvious, but you should say which facts they follow from (e.g. IH, definition, lemma X).
  • The questions will all be formal (you need not write an essay) but will not all be proofs but also function definitions, calculations etc.
• Please bring your laptop, with Isabelle 2016-1 installed, to the tutorials.

Material Material will be provided via a bitbucket repository, such that you can easily keep up to date. Lectures (and tutorial) will be recorded using the TTT tool. The recordings can be downloaded on the TTT Recordings Website (as soon as they have been processed and uploaded).

Exercises Exercise 1 , Theory developed in tutorial , Solution Exercise 2 , Theory developed in tutorial , Solution Exercise 3 , Theory developed in tutorial , Solution Exercise 4 , Theory developed in tutorial , Solution Exercise 5 , Template (ex and hw) , Tutorial thy , Solution Exercise 6 , Template (ex and hw) , Tutorial thy , Solution Exercise 7 , Template (ex and hw) , Tutorial thy , Solution Exercise 8 , Template (ex) , Template (hw) , Tutorial thy , Solution Exercise 9 , Template , Tutorial thy , Solution Exercise 10 , Template , Tutorial thy , Solution Exercise 11 , Template , Tutorial thy , Solution Exercise 12 , Template , Tutorial thy , Solution Exercise 13 , Template , Tutorial thy , Solution Exercise 14 , Template

Homework

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

• 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 40% towards the final grade.

Important notice

• You must be familiar with some functional programming language like Haskell, Objective Caml, Standard ML or F# (e.g. Introduction to Informatics 2 (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.
• At the end of the course there will be a written or oral examination, depending on the number of students. Throughout the course there will be homework assignments. They will involve the use of Isabelle and will be graded. The final grade will combine the grades from the examination (60%) and the homework (40%).
• All lectures are in English.

Literature

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

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