en | de

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: 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

Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof.
Morten Heine B. Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism.