Interactive Theorem Proving

master program

VO2 + PS3 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.