Concrete fully complete models of Linear Logic

Thomas Cuvillier

Linear logic is one of the most studied logics in theoretical computer science, especially from the denotational semantics point of view. Several important models, such as coherence spaces or games, have been first introduced as denotational models for linear logic, before being reused successfully for programming languages. The main goal of the present research is to find a concrete model that is also complete model; property described by Abramsky as "the tightest possible connection between syntax and semantics". Precisely, we want to avoid the use of 2-categorical tools to model type variables, together with not relying on a quotient. We hope that such a model could provide important insights for the study of linear logic, but also related and connected fields in semantics, such as semantics of programs and processes.

We will first recall the basics of Linear Logic, proof structures, and their associated categorical models. We present a new categorical construction mixing double-glueing and the Chu-construction. We build a relational semantics of proof structures based on permutations. We then use the new categorical construction to restrict the relation category and obtain full completeness for the multiplicative fragment without units. Moreover, our model can be enriched with a hypercoherence structure to yield a static fully complete model for the multiplicative additive fragment without units. This result allows us to prove a conjecture made by Pagani that relates hypercoherence and proof structures.