Parcours IL / Orientation MFLS
L’objectif de cette UE est d’étudier et de maîtriser les concepts et les techniques de construction de preuves dans des logiques non-classiques, utilisées en vue de modéliser et prouver des propriétés de programmes et de systèmes.
Prérequis
- Connaissances de base en logique.
Acquis d’apprentissage
- Logique classique et logiques non-classiques.
- Théorie de la démonstration:
- Déduction naturelle, calcul des séquents, preuves;
- Lambda calculs associés (normalisation, types).
- Logique intuitionniste
- Sémantique à la Kripke, sémantique de Heyting;
- Calculs
- Isomorphisme de Curry Howard, lambda-calcul
- Logiques modales et logique linéaire:
- Logiques modales : sémantique, axiomatisations et calculs;
- Logique linéaire : ressources, preuves, réseaux de preuve.
Compétences visées
- Maîtriser et mettre en œuvre 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.
- Maîtriser le raisonnement et la construction de preuves dans des logiques non-classiques utilisées pour la modélisation de concepts et de systèmes.
- Développer des systèmes de typage et d’inférence de types pour des langages.