### 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 | Additional lecture: HOL Light (pdf) | |||

2 | 14.10 Simple Type Theory | ||||

3 | 21.10 Gentzen, λ-properties | ||||

4 | 28.10 Principle Types | ||||

5 | 04.11 Introduction to λP | ||||

6 | 11.11 HOL packages | ||||

7 | 18.11 Lambda 2 | ||||

8 | 25.11 Paradoxes | ||||

9 | 02.12 Set theory intro | ||||

10 | 09.12 Mizar | ||||

11 | 16.12 Mizar, LF | ||||

12 | 13.03 Program Extraction | ||||

13 | 20.01 Isabelle | ||||

14 | 27.01 Presentations | ||||

15 | 03.02 First Exam |

### HOL Light

To install the small HOL-Light (10MB) on zid-gpl you need to:- wget http://cl-informatik.uibk.ac.at/~cek/hol_light.tgz
- tar xzf hol_light.tgz
- cd hol_light
- rlwrap ocaml
- #use "hol.ml";;
- (the hash symbol above # is necessary, it is different from the OCaml prompt)

### 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.