An explicit formula for the free exponential modality of linear logic

Abstract : The exponential modality of linear logic associates to every formula A a commutative comonoid !A which can be duplicated in the course of reasoning. Here, we explain how to compute the free commutative comonoid !A as a sequential limit of equalizers in any symmetric monoidal category where this sequential limit exists and commutes with the tensor product. We apply this general recipe to a series of models of linear logic, typically based on coherence spaces, Conway games and finiteness spaces. This algebraic description unifies for the first time a number of apparently different constructions of the exponential modality in spaces and games. It also sheds light on the duplication policy of linear logic, and its interaction with classical duality and double negation completion.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, 28 (7), pp.1253-1286. 〈10.1017/S0960129516000426〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01992148
Contributeur : Nicolas Tabareau <>
Soumis le : jeudi 24 janvier 2019 - 11:47:10
Dernière modification le : jeudi 7 février 2019 - 17:01:24

Lien texte intégral

Identifiants

Citation

Paul-André Melliès, Nicolas Tabareau, Christine Tasson. An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, 28 (7), pp.1253-1286. 〈10.1017/S0960129516000426〉. 〈hal-01992148〉

Partager

Métriques

Consultations de la notice

22