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.