Verified Functional Programming (WS 2023/24)


Instructor: Prof. Ralf Hinze

Teaching assistant: Michael Youssef


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

(for details about time and location updates see KIS)


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

(for details about time and location updates see KIS)


Please join our OLAT course to register.


Oral exams, details will be announced later.


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!