Sémantique, preuves et types

L’objectif de ce cours est de présenter lles 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 de contre-modèles.

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