Complex mathematical proofs on paper are difficult to write, check, and maintain. This holds not only for interesting proofs in mathematics, but also for complex formal proofs about interesting programs. For this reason, machine-checked proofs created with the help of interactive tools called proof assistants are gaining increased traction in academia and industry. Proof assistants have been used to prove the correctness and security of realistic compilers, operating systems, cryptographic libraries, or smart contracts, and also to construct machine-checked proofs for challenging mathematical results such as the four color theorem, the odd-order theorem (Feit–Thompson), or the construction of perfectoid spaces.

This course introduces the Coq proof assistant [2] and explains how to use it to prove properties about functional programs and inductive relations. The Coq proof assistant enables us to program formal proofs interactively and it machine-checks the correctness of the proofs along the way. The design of the Coq proof assistant itself exploits a beautiful connection between programs in typed functional programming languages and proofs in constructive logics, which is known as the Curry-Howard Correspondence [3]. This deep connection between programs and proofs should make this course interesting to both computer scientists and mathematicians. For computer scientists the goal is to demystify proofs as just programs in an elegant programming language, for which the course provides a gentle introduction. For mathematicians this course serves as an introduction to functional programming and also to the idea that proofs are not only a way to convince a human reader, but they can actually be fully formalized in a proof assistant like Coq and automatically checked by a computer.

This hands-on course is based on the Logical Foundations online textbook [1], which is itself formalized and machine-checked in the Coq proof assistant. The many exercises in each book chapter are to be solved weekly mostly in Coq, from easy exercises allowing the students to practice concepts from the lecture, building incrementally to slightly more interesting programs and proofs and also to various optional challenges. Finally, this course serves as the base for a more advanced course on “Foundations of Programming Languages, Verification, and Security”.

Learning Outcomes

After successful completion of this course, students will be able to

• develop purely functional programs using recursive functions on numbers, lists, maps, and various kinds of trees, including the abstract syntax trees of programs;
• use functional programming concepts such as type polymorphism and higher-order functions, which are increasingly becoming mainstream;
• formally state and prove theorems in the Coq proof assistant;
• apply different proof techniques in Coq (e.g. equational reasoning, contradiction, case analysis, induction on natural numbers, structural induction, proof automation);
• define new inductive types and relations in Coq and prove statements about them;
• understand the connection between constructive logics and typed functional programming that is at the heart of Coq, in which propositions are types and proofs are programs;
• understand how the syntax and semantics of simple imperative programs can be formally defined in Coq and how to prove theorems about such programs and languages.

Requirements for getting credit points

There will be a written final exam (120 minutes) that counts for 60% of the grade and weekly exercise sheets that have to be submitted on time and that count for 40% of the grade. We also plan to have a midterm exam that helps students practice for the final exam, but only counts for bonus points, up to 10% of the final grade. One can additionally get bonus points up to 5% of the final grade by solving all exercise sheets.

To pass the course and receive credit points the weighed sum of your scores including bonus points (which can add up to a maximum of 115%) has to be at least 50%.

Which students can attend this course and get official credit?

• Computer Science BSc students (and once the MSc program starts also MSc students)
• IT Security BSc and MSc students
• Mathematics MSc students ("Nebenfach Informatik")
• CASA PhD students -- attendance requirement is to reach 50% of the points in the exercise sheets (where because of bonus points the maximum is 112.5%)

eCampus page

• link

Literature

1. Benjamin C. Pierce et al. Software Foundations, Vol. 1: Logical Foundations
2. The Coq Proof Assistant
3. Philip Wadler: Propositions as types. Commun. ACM 58(12): 75-84 (2015)