Mécanisation de la preuve

L’objectif de ce cours est de présenter les concepts et méthodes concernant la mécanisation de la preuve.

Logiques, preuves et automatisation

  • principes de la preuve assistée/automatisée
  • logical frameworks (FOL, théorie des ensembles, type theory HOL, CiC )
  • principaux outils (Coq, Isabelle/HOL, PVS, Vampire…)

Les étapes de la mécanisation

  • choix de la logique (types de données, types de raisonnement, ordre supérieur)
  • modélisation du problème (implantation des types, expressions des lemmes)
  • construction de preuves (tactiques et stratégies, preuves par induction, généralisation, lemmes intermédiaires)
  • vérification des preuves (type checking)

Exemples/études de cas

  • présentation de quelques problèmes difficiles (protocole SSL/TLS, compilation certifiée CompCert )
  • étude de cas possibles (théorème de Ramsey, théorème du point fixe/bisimulation sémantique opérationnelle,logique de Hoare, complétude logique, élimination des coupures)