Logique, interaction et complexité (M2 PLS, cours, 2009-2010)

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).