nLab linear-non-linear logic

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.

Related

• 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

• Nick Benton, A mixed linear and non-linear logic: Proofs, terms and models, CSL 1994