HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Believe It Or Not, GOI is a Model of Classical Linear Logic

Jean Goubault-Larrecq 1
1 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We introduce the Danos-Régnier category $DR(M)$ of a linear inverse monoid $M$, a categorical description of geometries of interaction (GOI). The usual setting for GOI is that of a weakly Cantorian linear inverse monoid. It is well-known that GOI is perfectly suited to describe the multiplicative fragment of linear logic, and indeed $DR(M)$ will be a ∗-autonomous category in this case. It is also wellknown that the categorical interpretation of the other linear connectives conflicts with GOI interpretations. We make this precise, and show that $DR(M)$ has no terminal object, no cartesian product, and no exponential—whatever M is, unless M is trivial. However, a form of coherence completion of $DR(M)$ à la Hu-Joyal provides a model of full classical linear logic, as soon as $M$ is weakly Cantorian.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal.inria.fr/hal-03199716
Contributor : Jean Goubault-Larrecq Connect in order to contact the contributor
Submitted on : Thursday, April 15, 2021 - 8:47:06 PM
Last modification on : Friday, February 4, 2022 - 4:14:56 AM
Long-term archiving on: : Friday, July 16, 2021 - 7:18:52 PM

File

rr-lsv-2007-03.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03199716, version 1

Citation

Jean Goubault-Larrecq. Believe It Or Not, GOI is a Model of Classical Linear Logic. 2007. ⟨hal-03199716⟩

Share

Metrics

Record views

21

Files downloads

100