By restricting how variables can be used, we impose a linear (affine) type discipline.
Types act as resources, multiplicity matters.
Typically, sequent calculus, but various natural deduction style presentations.
It is illuminating to consider linearity in the context of natural deduction, since natural deduction simply-typed $\lambda$-calculus is the simplest example of the propositions-as-types correspondence.