Olivier Laurent
LIP, CNRS, ENS Lyon
http://perso.ens-lyon.fr/olivier.laurent/
Date(s) : 30/11/2017 iCal
11 h 00 min - 12 h 30 min
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.
Catégories