Information
- Lecturer : Kalmer Apinis (kalmer.apinis@ut.ee)
- Seminars : Thursdays, 16:15-17:30, Δ-2048, every two weeks,
- Homework : see Homework, submit to moodle
- Discussion : Fleep forum (log into courses to see link)
- Final exam:
- January 7th-8th or January 18th-19th
- open book e-exam (including the internet) + face-to-face Q&A if needed
- example
- Final grade
- max. 70 points for autograded HW (less if incorrect or submited late)
- max. 30 points for autograded exam+Q&A
- 0..50 → F, 51..60 → E, 61..70 → D, 71..80 → C, 81..90 → B, 91..100 → A
- Notes from Nov 5th seminar: notes.txt
Book recommendation
- Verified Functional Algorithms by Andrew W. Appel
- Logical Foundations by Benjamin C. Pierce et al
- "Certified Programming with Dependent Types", Adam Chlipala, 2019
- Program Logics for Certified Compilers by Andrew W. Appel et al., 2014
- Formal Reasoning About Programs by Adam Chlipala, 2017
- Computer Arithmetic and Formal Proofs by S. Boldo and G. Melquiond, 2017
- Binomial Queues by Andrew by W. Appel, 2016
- Efficient Verified Red-Black Trees by Andrew W. Appel, 2011
Preparation for the course
- We will be using Coq together with CoqIDE.
- Install Coq version 8.12.
- In Windows and OS X I suggest downloading CoqIDE from https://coq.inria.fr/download
- In Linux you can probably use a package manager.
What is interactive theorem proving
An interactive theorem prover such as Coq is a system where you can write propositions (such as "A ⋀ True → A") and prove them interactively. Proving something interactively means that the system keeps track of your goals as you apply logics rules and proof tactics. In the background, the system checks that the rules you have chosen are applicable and prohibits you to use rules that make no sense. This means that Coq proofs are machine-checked.
In this course we use the Coq system, but there are other similar tools. Coq can be used to formalize mathematics in general, but it can also be used for proving correctness of programs --- this fact makes Coq interesting for computer scientists.
Coq is not a toy or just a program that teaches students about logics. It is a mature tool that has 30 years of research behind it, which is actively used to for formalizing complicated proofs. Wikipedia lists its main achievements as
- Four color theorem: formal proof using Coq was completed in September 2004.
- Disjoint-set data structure: correctness proof in Coq was published in 2007.
- Feit–Thompson theorem: formal proof using Coq was completed in September 2012.
- CompCert: an optimizing compiler for a subset of the C programming language which is fully programmed and proved in Coq.
Forms of learning
You will learn by independently reading Logical Foundations and Verified Functional Algorithms and solving exercises in Coq. There will be a Fleep chat or some other online forum for cases where you get stuck with details. Also, there will be seminars every other week to better unerstand "the big picture".
The homework deadlines will have quite strict deadlines as extra motivation to not fall behind too much. This will allow you to help each other.
Scope of the course
No previous knowledge about proofs or Coq needed. We start at the beginning: the basics of Coq. Then we learn all required proof tactics and apply them to prove correctness of functional algorithms such as sorting, search trees, and priority queues. I am not obsessed with covering all chapters of "Verified Functional Algorithms" but we should aim to reach more than Red-Black tree operations.
Motivation for taking the course
- Being able to use interactive theorem provers (including Coq) is useful. There are highly paying jobs in Europe for writing provably correct software. Also, proving something interesting is a suitable topic for your PhD. Coq might never go mainstream, but provably correct software is the future. :-)
- Surprisingly few people in Estonia are using it. Stand out among your peers with an uncommon know-how/interests.
- As Coq is able to check your proofs, you get instant progress feedback on your course- and home-work. By solving all the exercises in timely manner, you are almost guaranteed to get a good result on the exam, as the exam is about proving similar theorems as in the practicals.
- You will get a better intuition about correct algorithms.
- You will be able to write provably correct code.