An explicit formula for the free exponential modality of linear logic - Archive ouverte HAL Access content directly
Journal Articles Mathematical Structures in Computer Science Year : 2018

An explicit formula for the free exponential modality of linear logic

(1) , (2, 3) , (1)
1
2
3

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.

Dates and versions

hal-01992148 , version 1 (24-01-2019)

Identifiers

Cite

Paul-André Melliès, Nicolas Tabareau, Christine Tasson. An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, 2018, 28 (7), pp.1253-1286. ⟨10.1017/S0960129516000426⟩. ⟨hal-01992148⟩
71 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More