Name
Abstract | ||
|---|---|---|
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 LPC structure. The paper's meta-theoretic 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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1017/S0960129516000347 | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE |
Field | DocType | Volume |
Discrete mathematics,Algebra,Duality (optimization),Category theory,Linear logic,Linear regime,Mathematics | Journal | 28 |
Issue | ISSN | Citations |
SP5 | 0960-1295 | 0 |
PageRank | References | Authors |
0.34 | 12 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jennifer Paykin | 1 | 0 | 1.01 |
| Stephan A Zdancewic | 2 | 0 | 0.34 |