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 de contre-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
- Maîtriser et mettre en oeuvre les méthodes formelles pour la spécification ou modélisation d’un problème donné, la preuve et la vérification de propriétés dans le contexte de la sûreté et la sécurité logicielle.
- Concevoir et développer des approches formelles adaptées, leur combinaison et des outils associés, pour la certification de systèmes complexes.
- 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.