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