Motivation
How can we ensure that software does not crash and is guaranteed to be correct? In this course we tackle this question by viewing programs and programming languages as mathematical objects. In this way we can use logic to prove properties about programs and thereby guarantee that software is correct. To make reasoning about actual programs and programming languages feasible, we will not be doing these proofs by hand, but instead use a tool called a proof assistant. Such tools help building proofs that can be checked by a computer. As we will show during this course, proof assistants turn the activity of doing proofs into programming.
Join our chat at https://quantumformalism.zulipchat.com/. We highly encourage you to join the chat so you can get the most out of the course!
The course's video content including mini lectures can be found on this YouTube playlist: https://www.youtube.com/watch?v=9kjld2Swg5w&list=PL6N_Y7ao_aHsHaECz813UGIvAGmrfrOYX&pp=iAQB.
Introduction
- Presentation of the learning material
- Explanation of learning mode: flipped classroom
- Means of contact (git repository, Zulip chat)
- Introduction to Lean
Propositional logic
- Logic of statements https://en.wikipedia.org/wiki/Propositional_calculus
- Study of logical operations "and", "or", and implication
- Proofs of propositions in natural deduction style https://en.wikipedia.org/wiki/Natural_deduction
Predicate logic aka first order logic
- Study of quantifiers, universal ("for all") and existential ("there exists")
- https://en.wikipedia.org/wiki/First-order_logic
Functional programming and verification
- Programming style supported in Haskell, Ocaml, Python, etc, https://en.wikipedia.org/wiki/Functional_programming
- Functional programs are particularly well-suited for formal verification
- Lean supports functional programming natively
Use of a computer proof assistant
- Computer proof assistants provide a language suitable for both programming and proving: an algorithm can be both implemented and proved correct in the same language.
- Computer proof assistants check the correctness of user-provided proofs.
- Programs can be executed directly in the computer proof assistant.
TBA
For every week, a workplan for you is specified on the dedicated page:
The workplans will be provided on a rolling basis.
- Book Logic and Proof
- Course Logical Verification
- Textbook
- Git repository with Lean files
- Lecture videos are available on Logical Verification