After successful completion of the course, you will be able to:
- Give mathematical models of imperative and concurrent programming languages using operational semantics.
- Prove properties of imperative and concurrent programs using separation logic.
- Prove properties of type systems for imperative and concurrent programming languages.
- Use the Coq proof assistant to carry out mechanized proofs about program language semantics, separation logic, and type systems.
How can we formally ensure that a program satisfies certain properties? For example, that it does not have memory bugs (such as null-pointer accesses, use-after-free, or buffer overflows) or concurrency bugs (such as data races or deadlocks), that it does not leak confidential information (such as passwords or personal information), or that its output adheres to some mathematical specification?|
In this course we study two formalisms to prove such program properties:
In this course, we use the Coq proof assistant to implement and develop the theory of these formalisms, and apply them to sample programs. In the first three weeks of the course, we will study the basics of Coq, to lay the groundwork for the rest of the course.
- Types. Many programming languages classify program expressions using types, and thereby automatically rule out ill-behaved programs like `true + 10`. Modern programming languages like Rust use types to ensure that programs are free of much larger classes or bugs, like memory and concurrency bugs.
- Logic. Using logic one can specify and prove arbitrarily complicated properties of programs. To scale this up to imperative and concurrent programs, we study the formalism of concurrent separation logic (for which the inventors Brookes and O'Hearn received the 2016 Gödel price).
- Prior knowledge of functional programming (e.g., NWI-IBC040 "Functional Programming") and semantics (e.g., NWI-IBC026 "Semantics and Correctness" and NWI-IBC025 "Semantics and Rewriting") is required.|
- Prior knowledge of concurrency is not required.
- Having taken the course NWI-IMC010 "Type Theory and Coq" is beneficial, but not required. The present course uses Coq to study imperative programming languages with concurrency, whereas NWI-IMC010 studies the foundations of Coq in the context of lambda calculus, type theory, and the formulas-as-types correspondence. All Coq exercises in this course are self-contained and different from those in NWI-IMC010.
The final grade is based on the following parts:|
- An end-project in the Coq proof assistant
- A written exam.
Both parts have a weight of 50%, and the grade for both parts should be at least a 5.