nLab linear-non-linear logic

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Monoidal categories

monoidal categories

With symmetry

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

Contents

Idea

Linear-non-linear logic is a presentation of intuitionistic linear logic that decomposes the !! modality into an adjunction of between a syntax for a cartesian logic and a linear logic with cartesian variables.

The semantics of linear-non-linear logic is more direct than that of intuitionistic linear logic: it is based on a symmetric monoidal adjunction where the source of the left adjoint is a cartesian monoidal category.

  • If the linear context is restricted to having at most one variable, the judgmental structure of linear-non-linear logic coincides with call-by-push-value with stacks.

References

Created on April 20, 2018 at 18:00:38. See the history of this page for a list of all contributions to it.