Logique, interaction et complexité (M2 PLS, cours, 2009-2010)
-
fichiers : pdf
2009-2010
Je partage avec Jean-Yves Moyen la responsabilité du cours d’approfondissement logique, interaction et complexité du master 2 PLS (programmation et logiciels sûrs).
Logique linéaire : calcul des séquents, représentation géométrique des preuves, critères de correction et théorème de séquentialisation, interaction et interprétation de programmes.
Programmation par preuves : principe de résolution, normalisation des preuves de la logique linéaire et application à la programmation, notion de polarisation.
Complexité implicite pour la programmation fonctionnelle : vérification et caractérisation (Ptime, Pspace, ...) par le typage (logique linéaire), par ordre de terminaison et interprétation (quasi-interprétations).