burkhart.wolff

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 2020 is tentative !!!

• C1 5.1. 14:00-17:30 [D203]:
  Introduction, motivations, simply-typed λ-calculus.

  
  

  TP1: Getting familiar with Isabelle/HOL and PIDE.

  • 00:00:22 Overall Motivation: Why ITPs ?
  • 00:03:37 Untyped λ-terms
  • 00:12:14 Conversions and Reductions
  • 00:29:12 The typed λ-calculus
  • 00:48:08 Properties of the typed λ-calculus
  • 00:53:04 Encoding logics in the typed λ-calculus
  • 00:53:49 Outlook: Representing natural deduction rules
  
  

• C2 12.1. 14:00-17:30 [D203]: Higher-order logics and elementary proofs.

  
  

  TP2: Datatypes and Induction in Isabelle/HOL

  • 00:01:35 Context and Motivation
  • 00:20:14 Foundations : Deduction
  • 00:27:45 Deduction Rules for HOL
  • 00:36:00 Formal Proofs
  • 00:48:18 Proof Construction
  • 00:55:50 Apply-style Proofs in Isabelle
  
  

• C3 19.1. 14:00-17:30 [D203]: HOL Semantics, Conservative Definitions, Inductive Data-Types, Recursive Definitions.

  
  

  TP3: Specification Constructs in Isabelle

  • 00:02:11 Front-End: Isabelle's Document Model
  • 00:04:07 Back-End: Global/Local Contexts and Extensions
  • 00:13:25 HOL Semantics and Foundations
  • 00:40:21 Conservative Extensions of Contexts
  • 00:59:40 Specification Constructs in Isabelle/HOL
  • 00:12:23 More on Proof Automation
  
  

• C4 26.1. 14:00-17:30 [D203]: Inductive Proofs, Case Distinctions, and an Introduction to Structured Proofs in Isar.

  
  

  TP4: Inductive Constructs in Isabelle

  • 00:02:45 Inductive Sets and lfp-Fixed Points revisited
  • 00:41:50 Induction and Case-Distinctions considered logically
  • 00:46:40 Induction and Cases in Isabelle
  • 00:49:25 Introduction to Structured Proofs in Isar
  
  

• C5 2.2. 14:00-17:30 [D203]: Proof-Automation: An Introduction.

  
  

  TP5: Inductive Constructs for Modeling Regular Languages

  • 00:02:40 Revision: Imperative and Declarative Proofs
  • 00:06:50 Revision: Elementary apply-style (backward) proofs
  • 00:09:45 New: Elementary attributed (forward) proofs
  • 00:12:08 Revision: Advanced apply-style induction and case-splitting
  • 00:16:25 Rewriting
  • 00:36:50 Tableaux provers
  • 00:41:50 Paramodulation prover
  • 00:46:40 Presburger arithmetics prover
  • 00:48:22 A magic device: sledgehammer
  
  

• C6 9.2. 14:00-17:30 [D203]: Application: Formally Verifying a Micro-Kernel: Experiences from the seL4 Project .
  

  TP6: Modeling an Operational Semantics Inductively
  

• Regular Language Project, Regular Language Description.

Examen 16.2.2021 : 14 - 17:30 SALLE PUIO D101. :

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

Downloads:

• current version (Use Version 2020!), 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.