en | de

Interactive Theorem Proving

master program

VO3 + PS2  WS 2016/2017  703640 + 703641

Content

The interactive theorem proving lecture introduces the design of an LCF prover; formal proofs; structured proofs and proof scripts; higher-order logic: induction, recursive data structures and recursive functions; automation; termination proofs; correctness of programs.

The proseminar allows for deepened understanding of interactive theorem proving through training with established theorem provers; practicing through case studies of programs from different domains; working on a larger verification project.

Schedule

week topics slides exercises homework solutions
1 07.10 Proof Assistants pdf Additional lecture: HOL Light (pdf)
2 14.10 Simple Type Theory pdf pdf
3 21.10 Gentzen, λ-properties pdf
4 28.10 Principle Types pdf pdf pdf
5 04.11 Introduction to λP pdf pdf
6 11.11 HOL packages pdf pdf pdf
7 18.11 Lambda 2 pdf pdf pdf
8 25.11 Paradoxes pdf
9 02.12 Set theory intro pdf pdf
10 09.12 Mizar pdf pdf
11 16.12 Mizar, LF pdf pdf
12 13.03 Program Extraction pdf pdf pdf
13 20.01 Isabelle pdf pdf
14 27.01 Presentations
15 03.02 First Exam

HOL Light

To install the small HOL-Light (10MB) on zid-gpl you need to: If you want to use in on your own computer, follow the instructions from here.

Mizar

Recommended Reading Materials

Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof.
Morten Heine B. Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism.