Une promenade entre logiques linéaires classiques et intuitionnistes

Carte non disponible

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/

Olivier CHABROL
Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange