en | de

# Interactive Theorem Proving

## master program

VO3 + PS2  SS 2013  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.

The following schedule is temporary.

### Schedule

week topics slides exercises homework
1 08.03 Proof Assistants pdf 14.03 (Additional Lecture) HOL Light
2 15.03 λ-Calculus and STT pdf 21.03 HOL Light Rules pdf
3 22.03 Principal Types pdf 11.04 Tactics pdf
4 12.04 Dependent Types and λP pdf 18.04 λP and Tactics pdf
5 19.04 λP, Conversions pdf 25.04 Curry Howard for λP pdf
6 26.04 Polymorphism, λ2 pdf 02.05 λP, λ2 pdf
7 03.05 Set Theory pdf 16.05 Quotient types pdf
8 17.05 Declarative Proof pdf 23.05 Nominal and Mizar basics (.miz) pdf
9 24.05 Mizar pdf (holiday)
10 31.05 Code Extraction/Generation pdf 06.06 Mizar (s_1,s_2,tran1,fdemo_1) pdf
11 06.06 Isabelle and LFs pdf 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"
If you want to use in on your own computer, follow the instructions from here.

### 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
If you want to use it on your own computer, get Mizar 8.