en | de

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: 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: If you want to use it on your own computer, get Mizar 8.

Recommended Reading Materials

Morten Heine B. Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism.