Interactive Theorem Proving

master program

VO2 + PS3 SS 2015 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
1	03.03 Proof Assistants	pdf	09.03 HOL Light lecture (slides)
2	10.03 λ-Calculus and STT	pdf	16.03 HOL Light Rules	pdf
3	17.03 Intuitionistic logic, Gentzen Style	pdf	23.03 Tactics and Subgoal package	pdf
4	24.03 Principal Types, λ-cube	pdf	13.04 Minimal Kernel, Tactical proofs	pdf
5	14.04 λP, Conversions	pdf	20.04 Curry Howard for λP	pdf
6	21.04 HOL libraries	pdf	27.04 λP, introducing types	pdf
7	28.04 Polymorphism, λ2	pdf	04.05 λ2	pdf
8	05.05 Set Theory	pdf	11.05 Flag type derivations	pdf
9	12.05 Declarative Proof	pdf	18.05 Mizar	pdf
10	19.05 Coq	pdf	(holiday)
11	26.05 Code extraction and generation	pdf	01.06 Coq	pdf
12	02.06 Logical Frameworks	pdf	08.06 Encoding	pdf
13	09.06 λHOL and extensions	pdf	15.06 ACL2, Plastic, Imps
14	16.06 MetaMath, MinLog
15	29.06 First Exam 8:00 3W04,

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

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.