Interactive Theorem Proving

master program

VO2 + PS3 WS 2016/2017 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.

Schedule

week	topics	slides	exercises	homework	solutions
1	07.10 Proof Assistants	pdf	Additional lecture: HOL Light (pdf)
2	14.10 Simple Type Theory	pdf		pdf
3	21.10 Gentzen, λ-properties	pdf
4	28.10 Principle Types	pdf		pdf	pdf
5	04.11 Introduction to λP	pdf		pdf
6	11.11 HOL packages	pdf		pdf	pdf
7	18.11 Lambda 2	pdf		pdf	pdf
8	25.11 Paradoxes			pdf
9	02.12 Set theory intro	pdf			pdf
10	09.12 Mizar	pdf		pdf
11	16.12 Mizar, LF	pdf		pdf
12	13.03 Program Extraction	pdf		pdf	pdf
13	20.01 Isabelle	pdf		pdf
14	27.01 Presentations
15	03.02 First Exam

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)

If you want to use in on your own computer, follow the instructions from here.

Mizar

Get Mizar 8
Set environment variables like the install tells you to
example .emacs file