Master Seminar: Functional Programming and Type Theory

Instructor: Luca Maio

Content

Functional programming has many advanced applications but most share one thing: they rely on a strong type system. This ensures a level of safety and correctness not easily achievable by imperative means. Further, dependent type theories can even be used to model mathematics as a whole and thus have computers check or even find proofs of real mathematical theorems. Interactive proof assistants such as Agda, Coq, Lean, and Matita are based on dependent type theory. After a short introduction to type theory, you will pick a topic in advanced functional programming or (dependent) type theory for your seminar paper and talk.