This course is a self-contained introduction to the proof assistant Isabelle/HOL. It is based on the first part of the book by Prof. Tobias Nipkow and Prof. Gerwin Klein,
which is available both as a free PDF online and as a hardcover from
Springer. Several exercise will be about reasoning on first order and
propositional logic.
Proof assistants are tools that allow its users to carry out mathematical proofs rigorously, based on a logical foundation. Developing a proof in a proof assistant as opposed to using pen and paper is roughly the equivalent of programming on a computer as opposed to sketching pseudo-code on paper. Expertise with proof assistants is becoming an increasingly important skill, especially for software verification, which aims at proving the absence of bugs in programs. In the experience of many instructors, the use of a proof assistant helps students get a good grip on computer science topics.
Coq and Isabelle are the main two proof assistants in use. Isabelle's strength is that it is simple as 1-2-3: It offers (1) a simple yet powerful logic, (2) a convenient user interface, and (3) a lot of proof automation.
There are no formal prerequisites for taking the course. Familiarity with a typed functional programming language (such as Standard ML, OCaml, Haskell, or F#) is highly recommended.
- theorem proving is too addictive for you;
- you want to trust you own paper proofs;
- you never understood how induction works.
UPDATE: The university has presented the COVID rules. Only 20 stundents are
allowed to be in the room we are currently scheduled in. Unless too many student register, teaching will happen as follows: if the `ampel' is green or yellow, no remote. Otherwise (or if masks become mandatory in the rooms), teaching will be purely remote (no hybrid).
- Teacher: Mathias Fleury