The Sup Connective in IMALL: A Categorical Semantics
Logic in Computer Science
2026-04-03 v5 Category Theory
Logic
Abstract
We explore a proof language for intuitionistic multiplicative additive linear logic, incorporating the sup connective that introduces additive pairs with a probabilistic elimination, and sum and scalar products within the proof-terms. We provide an abstract characterisation of the language, revealing that any symmetric monoidal closed category with biproducts and a monomorphism from the semiring of scalars to the semiring Hom(I,I) is suitable for the job. Leveraging the binary biproducts, we define a weighted codiagonal map which is at the core of the sup connective.
Keywords
Cite
@article{arxiv.2205.02142,
title = {The Sup Connective in IMALL: A Categorical Semantics},
author = {Alejandro Díaz-Caro and Octavio Malherbe},
journal= {arXiv preprint arXiv:2205.02142},
year = {2026}
}