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

1 | 03.03 Proof Assistants | 09.03 HOL Light lecture (slides) | ||

2 | 10.03 λ-Calculus and STT | 16.03 HOL Light Rules | ||

3 | 17.03 Intuitionistic logic, Gentzen Style | 23.03 Tactics and Subgoal package | ||

4 | 24.03 Principal Types, λ-cube | 13.04 Minimal Kernel, Tactical proofs | ||

5 | 14.04 λP, Conversions | 20.04 Curry Howard for λP | ||

6 | 21.04 HOL libraries | 27.04 λP, introducing types | ||

7 | 28.04 Polymorphism, λ2 | 04.05 λ2 | ||

8 | 05.05 Set Theory | 11.05 Flag type derivations | ||

9 | 12.05 Declarative Proof | 18.05 Mizar | ||

10 | 19.05 Coq | (holiday) | ||

11 | 26.05 Code extraction and generation | 01.06 Coq | ||

12 | 02.06 Logical Frameworks | 08.06 Encoding | ||

13 | 09.06 λHOL and extensions | 15.06 ACL2, Plastic, Imps | ||

14 | 16.06 MetaMath, MinLog | |||

15 | 29.06 First Exam 8:00 3W04, |

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

On zid-gpl is in /usr/site/mizar. To set up the environment do:- export MIZFILES=/usr/site/mizar/8.1.01/i386/share/mizar/
- export PATH=/usr/site/mizar/8.1.01/i386/bin:$PATH
- example .emacs file

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