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

The following schedule is temporary.

### Schedule

week | topics | slides | exercises | homework |
---|---|---|---|---|

1 | 08.03 Proof Assistants | 14.03 (Additional Lecture) HOL Light | ||

2 | 15.03 λ-Calculus and STT | 21.03 HOL Light Rules | ||

3 | 22.03 Principal Types | 11.04 Tactics | ||

4 | 12.04 Dependent Types and λP | 18.04 λP and Tactics | ||

5 | 19.04 λP, Conversions | 25.04 Curry Howard for λP | ||

6 | 26.04 Polymorphism, λ2 | 02.05 λP, λ2 | ||

7 | 03.05 Set Theory | 16.05 Quotient types | ||

8 | 17.05 Declarative Proof | 23.05 Nominal and Mizar basics (.miz) | ||

9 | 24.05 Mizar | (holiday) | ||

10 | 31.05 Code Extraction/Generation | 06.06 Mizar (s_1,s_2,tran1,fdemo_1) | ||

11 | 06.06 Isabelle and LFs | 20.06 Automath, Minlog, Agda | ||

12 | 21.06 Lego, PVS | |||

13 | 02.07 Exam 1 |

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

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