Beschreibung von Proofs are Programs (211003-WiSe 2024/25)

Proofs are Programs (211003-WiSe 2024/25)

Time and Location

Lecture: Thursdays, 10:00 AM - 12:00 PM (from 10 Oct to 30 Jan)
- The location of the lecture will be announced soon.
- For everyone's benefit, we would like this to remain a mostly in-person course, so to get the best out of it, we encourage everyone to attend the lecture physically whenever possible. When you cannot attend the lecture in person there will be the Zoom room you can use.
Exercise sessions: Wednesdays, 2:00 PM - 4:00 PM (from 16 Oct to 29 Jan)
- The exercise sessions will take place in person in building MB, floor 5, room SM-MO-506 (an MPI-SP seminar room). Building MB was formerly also known as Technologiezentrum Ruhr (or TZR). Please enter via the main MB entrance, which faces the MC building and the parking lots between MC and MB. Then take the glass elevator right next to the entrance or the stairs up to floor 5. On floor 5 enter the open door of the Max Planck Institute for Security and Privacy (MPI-SP) and the seminar room is only a few steps away. Should the MPI-SP door be closed, please ring the bell and someone will open for you.

Course Description

Complex proofs on paper are difficult to construct, 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 theorems in mathematics.

This course introduces the Coq proof assistant [3] and explains how to use it to prove properties about functional programs and inductive relations, how to formally define a simple imperative programming language, and how to securely enforce information-flow control for functional and imperative programs. 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 [4]. This deep connection between programs and proofs should make this course interesting to not only to computer scientists, but also to mathematicians and other scientists. The goal is to demystify proofs as just programs in an elegant programming language, for which the course provides a gentle introduction. The course also shows 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 [1] and Security Foundations [2] online textbooks, which are themselves 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”.

No Prerequisites

The lecture is intended for a broad range of students, from motivated BSc students to MSc and PhD students. No specific prior knowledge in logic, programming, functional programming, or programming languages is assumed, though a degree of mathematical maturity is helpful.

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, lists, and trees, induction on rule derivations, proof automation);
define new inductive types and relations in Coq and prove statements about them;
write simple proof terms and 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;
comprehend 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;
understand how the absence of information leaks can be formalized as a security property called noninterference and enforced using secure-multi execution or simple type systems.

Requirements for getting credit points

There will be a mandatory written final exam (120 minutes) that counts for 100% of the grade. In addition there will be weekly exercise sheets that have to be submitted on time and that count for bonus points, up to 20% of the final grade. We will also have an optional midterm exam that helps students practice for the final exam, but only counts for bonus points, up to 10% of the final grade.

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

Literature

[1] Benjamin C. Pierce et al. Software Foundations, Vol. 1: Logical Foundations: https://softwarefoundations.cis.upenn.edu/lf-current/index.html

[2] Catalin Hritcu and Roberto Blanco. Security Foundations: https://mpi-sp-foe-2023-24.github.io/book-secf/

[3] The Coq Proof Assistant: https://coq.inria.fr

[4] Philip Wadler: Propositions as types. Commun. ACM 58(12): 75-84 (2015) https://doi.org/10.1145/2699407

Kursinformation