Sémantique, preuves et types

Parcours IL / Orientation MFLS

L’objectif de ce cours est de présenter les liens entre preuves,types et programmes au travers de l’isomorphisme de Curry-Howard et des lambda-calculs typés. Dans ce contexte on étudiera un certain
nombre de logiques sous-structurelles et de logiques de ressources du point de vue de la sémantique et de la théorie de la preuve en présentant des concepts et méthodes adaptées de recherche de preuves
et de réfutations avec un intérêt fort pour la génération decontre-modèles.

Pré-requis

  • Connaissances de base en logique.

Acquis d’apprentissage

  • Logiques sous-structurelles :
    * logique intuitionniste, logiques de ressources;
    * sémantiques et calculs avec ou sans labels.
  • Preuves et Types:
    * isomorphisme de Curry-Howard;
    * lambda-calculs typés, preuves et programmes.
  • Preuves et réfutations
    * complétude par recherche de preuves;
    * structures sémantiques et calculs;
    * génération de contre-modèles.

Compétences visées

  • Développer des systèmes de preuves en lien avec la programmation.
  • Construire des contre-modèles en vue d’analyser l’échec de la vérification formelle de
    certaines propriétés de programmes.

Parcours IL / Orientation MFLS