Une promenade entre logiques linéaires classiques et intuitionnistes

Carte non disponible
Speaker Home page :
Speaker :
Speaker Affiliation :

()

Date/heure
Date(s) - 30/11/2017
11 h 00 min - 12 h 30 min

Catégories


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.

http://perso.ens-lyon.fr/olivier.laurent/


Retour en haut 

Secured By miniOrange