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 | 09.03 HOL Light lecture (slides) | ||
2 | 10.03 λ-Calculus and STT | 16.03 HOL Light Rules | ||
3 | 17.03 Intuitionistic logic, Gentzen Style | 23.03 Tactics and Subgoal package | ||
4 | 24.03 Principal Types, λ-cube | 13.04 Minimal Kernel, Tactical proofs | ||
5 | 14.04 λP, Conversions | 20.04 Curry Howard for λP | ||
6 | 21.04 HOL libraries | 27.04 λP, introducing types | ||
7 | 28.04 Polymorphism, λ2 | 04.05 λ2 | ||
8 | 05.05 Set Theory | 11.05 Flag type derivations | ||
9 | 12.05 Declarative Proof | 18.05 Mizar | ||
10 | 19.05 Coq | (holiday) | ||
11 | 26.05 Code extraction and generation | 01.06 Coq | ||
12 | 02.06 Logical Frameworks | 08.06 Encoding | ||
13 | 09.06 λHOL and extensions | 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)
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
Recommended Reading Materials
Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof.Morten Heine B. Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism.