Verified Functional Programming (WS 2022/23)

Organization

Instructor: Prof. Ralf Hinze

Teaching assistant: Michael Youssef

Lecture

  • Tuesday, 15:30 - 17:00, 48-453
  • Wednesday, 13:45 - 15:15, 48-453

(for details see KIS)

Exercises

  • Thursday, 15:30 - 17:00, 48-379

(for details see KIS)

Registration

Please join our OLAT course to register.

Exams

Oral exams, details will be announced later.

Overview

Verified Functional Programming takes the content of the Functional Programming lectures to the next level. The course aims to introduce concepts such as the following

  • Advanced Types Systems
  • Interactive Theorem Proving
  • Constructive Higher-Order Logic

To introduce these concepts, we will use Agda, a functional programming language with an advanced type system that allows us to model programs alongside proving properties about them.

Topics include, but are not limited to.

  • type-driven program development;
  • correctness of algorithms (sorting, Huffman coding);
  • dependent types
  • data structures and their invariants (searching)
  • partiality and termination
  • compiler construction
  • programming language foundations
  • propositional logic
  • inductive and coinductive types
  • formal languages
  • order theory

The format of the lecturers will be highly interactive: we will jointly develop programs and proofs. So, do bring your laptop along, ideally with Agda pre-installed!