02/10/2008 Olivier Laurent (ENS Lyon)

Un modèle de jeux quantitatif de la logique linéaire intuitionniste

Partant du travail d'Ugo Dal Lago sur la geometrie de l'interaction (LICS 06) et de la notion de cout introduite dans les "Slot games" par Dan Ghica (POPL 05), on definit un modele de jeux de IMELL sensible au temps de normalisation des preuves. A toute strategie interpretant une preuve, on associe alors une mesure de complexite en composant la strategie avec une strategie TA (analyseur de temps) qui ne depend que de la formule prouvee. La mesure ainsi obtenue est polynomialement reliee au nombre d'etapes necessaire pour normaliser la preuve. [travail en collaboration avec Ugo Dal Lago]