zbMATH — the first resource for mathematics

Multiplexor categories and models of soft linear logic. (English) Zbl 1132.03352
Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 472-485 (2007).
Summary: We give a categorical interpretation of Lafont’s Soft Linear Logic, a logical system complete for polynomial time computation, in terms of multiplexor categories. We present two main classes of models and methods for constructing examples in each case. As a concrete example of the first type, we introduce a simple game semantics for Multiplicative Soft Linear Logic. To illustrate the second type, we give a realizability model and a new proof of the polytime soundness of Soft Linear Logic. These results further our semantic understanding of Soft Linear Logic and polynomial time.
For the entire collection see [Zbl 1121.03005].

03F52 Proof-theoretic aspects of linear logic and other substructural logics
Full Text: DOI