2015/02/17 by Jennifer Paykin, Steve Zdancewic
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.176.2
published as EPTCS 176, 2015, pp. 9-23 · In Proceedings LINEARITY 2014, arXiv:1502.04419
arxiv created 2015/02/17 · arxiv updated 2015/02/18
This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions reflecting the linear/producer/consumer structure. The paper's metatheoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into category theory. The work also presents several concrete instances of the LPC model.