MPRI M1 Course:
Interactive Theorem Proving and Applications
("Introduction aux assistants de preuve")

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.
ecampus site
ecampus visio link (default)
jitsi visio link (reserve)
Calendrier

The Material from Spring 20201 is tentative !!!


Examen TO BE ANNOUNCED :

Project Resume due: 15.3. (submit electronically to ~wolff@lri.fr !) Project Description. Project Sources.

Downloads:

  • current version (Use Version 2022!), Earlier Isabelle Versions
  • The Isabelle Archive of Formal Proofs (AFP)



  • 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 documentation coming with Isabelle..
    • The Reference for HOL-Foundations:
      [4] Peter B. Andrews: An Introduction to Mathematical Logic and Type Theopry --- To Truth Through Proof. Springer 2002. (I still prefer the 1986-version...)
    • The Reference for a Standard Model of HOL and Conservative Extensions:
      [5] Mike Gordon and Tom Melham (eds): An Introduction to HOL, a Theorem Proving Environment for Higher Order Logic. 1994.