Formulae-as-Types for an Involutive Negation

Résumé : La négation n'est pas involutive dans le calcul λC car celui-ci échoue à distinguer les piles capturées des continuations. On montre qu'il y a une correspondance " formule pour type " entre la négation involutive de la théorie de la démonstration, et une notion d'accès de haut niveau aux piles étudiée par Felleisen et Clements. On introduit des calculs polarisés, non typés, compatibles avec l'extensionnalité, à la fois pour le calcul des séquents classique et le déduction naturelle classique, avec des connecteurs pour une négation involutive. L'involution est due à l'opérateur de contrôle délimité ℓ qu'on introduit, qui permet d'implémenter l'idée que les piles capturées, contrairement aux continuations, peuvent être inspectées. Délimiter le contrôle donne par ailleurs une interprétation constructive à l'absurdité. On décrit les isomorphismes qu'il y a entre A et ¬¬A, et par conséquent entre ¬∀ et ∃¬.
Type de document :
Communication dans un congrès
Joint meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS 2014), Jul 2014, Vienna, Austria. 2014, 〈10.1145/2603088.2603156〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00996742
Contributeur : Guillaume Munch-Maccagnoni <>
Soumis le : lundi 14 juillet 2014 - 02:18:24
Dernière modification le : vendredi 26 janvier 2018 - 13:26:02
Document(s) archivé(s) le : vendredi 21 novembre 2014 - 14:23:37

Fichier

involutive.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Guillaume Munch-Maccagnoni. Formulae-as-Types for an Involutive Negation. Joint meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS 2014), Jul 2014, Vienna, Austria. 2014, 〈10.1145/2603088.2603156〉. 〈hal-00996742v2〉

Partager

Métriques

Consultations de la notice

323

Téléchargements de fichiers

112