FIIL Course: Interactive Theorem Proving and Applications
("Preuves Interactives et Applications")
Objective:
Interactive Theorem Proving is a technology of growing importance in computer
science and mathematics. It is based on powerful logical languages with a strong
expressivity and implementations allowing to establish a high degree of
confidence in the correctness of the results. Among the applications, the
mechanically checked proof of the Feit-Thomson theorem can be noted, as well as
a correctness proof of the seL4 system, a secured operating system micro-kernel
in the L4 tradition.
This course is an introduction into the fundamentals of interactive proof environments and will be practically illustrated with the Isabelle/HOL system. The examples will address problems of modelling and proof and will introduce into the techniques to proof properties of languages or systems. It gives also an introduction into some of the foundations of mathematics and computer science.
Goal: Getting practical experience for modeling and proving with interactive theorem proving environments. Units will usually take place at Bat. 640,14:00 - 17:30, room E105. They consist of a course and a following TP. At the end of the course, a small project will be developped individually which will become the grade for CC, which counts 40 percent.
The Material from 2019 is tentative !!!
Downloads :
Project Resume due: 30.1. (submit electronically to ~wolff@lri.fr !)
This course is an introduction into the fundamentals of interactive proof environments and will be practically illustrated with the Isabelle/HOL system. The examples will address problems of modelling and proof and will introduce into the techniques to proof properties of languages or systems. It gives also an introduction into some of the foundations of mathematics and computer science.
Goal: Getting practical experience for modeling and proving with interactive theorem proving environments. Units will usually take place at Bat. 640,14:00 - 17:30, room E105. They consist of a course and a following TP. At the end of the course, a small project will be developped individually which will become the grade for CC, which counts 40 percent.
The Material from 2019 is tentative !!!
- C1 11. 9. [E105]: Introduction, motivations, simply-typed lambda-calculus.
- C2 16. 9. 13:00 - 16:15 [E105]: Higher-order logics, terms in HOL, elementary proofs.
Isabelle Intro TP1
demo1
demo2
Induction.thy
- C3 25. 9 [E105]: Conservative Definitions, Inductive Data-Types, Recursive Definitions, Inductive Proofs (1). TP2, TP2Solution.
- C4 2. 10 [E105]: Recursive Functions, Inductive Proofs, Intro ISAR(2). TP3,
- C5 16.10. [E105]: Proof-Automation: Unification, Rewriting. TP4, TP3Solution.
- C6 22.10. [E105]: Structured Proof Techniques . TP5Solution.
- C7 23.10. [E105]: Advanced Application: The seL4 Project AutoCorres Demo
- Examen 12.11. (?? TO BE CONFIRMED ??)[E105] :
Downloads :
- current version (Use Version 2019!) Isabelle Earlier Versions, and
- Choose one of these projects:
Project Resume due: 30.1. (submit electronically to ~wolff@lri.fr !)
Bibliography:
- [0] van Dalen, Dirk: Logic and Structure. THE REFERENCE ON NATURAL DEDUCTION. Online here.
- [1]Nipkow, Tobias, Paulson, Lawrence C., Wenzel, Markus : Isabelle/HOL A Proof Assistant for Higher-Order Logics. Lecture Notes in Computer Science, Vol. 2283. 2002. (quite outdated)
- [2] Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle Framework. In TPHOLs, pages 33 - 38, 2008.
- [3] Documentation (highly recommended): comes with the download of the current version.