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.
Document type :
Journal articles
Liste complète des métadonnées

https://hal.inria.fr/hal-01992148
Contributor : Nicolas Tabareau <>
Submitted on : Thursday, January 24, 2019 - 11:47:10 AM
Last modification on : Thursday, April 4, 2019 - 1:23:40 AM

Links full text

Identifiers

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⟩

Share

Metrics

Record views

32