Verified Functional Programming (WS 2023/24)
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 about time and location updates see KIS)
Exercises
- Thursday, 15:30 - 17:00, 48-379
(for details about time and location updates 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!
