Exposés

11:00: Olivier Laurent (LIP, ÉNS Lyon), Une promenade entre logiques linéaires classiques et intuitionnistes

On s'intéresse à différentes manières de relier la logique linéaire classique (LL) et sa version intuitionniste (ILL). Les principaux ingrédients sont l'étude de non-non traductions de LL dans ILL, et les résultats de conservativité de LL sur ILL. En analysant le cas particulier d'une non-non traduction bien choisie de LL dans TL (la logique tensorielle, fragment "positif" de ILL), on montre que l'on peut re-prouver la propriété de focalisation de LL. Cette preuve établit un lien entre les caractéristiques "au plus une formule à droite" des systèmes intuitionnistes et "au plus une formule positive active" des systèmes focalisés.

Ces différents résultats ont été formalisés en Coq à l'aide de la bibliothèque Yalla. Nous présenterons brièvement cette bibliothèque, ses spécificités et la manière de l'utiliser.