Linear type system

Definition

Take the types $\tau ::= b \mid \tau \multimap \tau \mid \tau \otimes \tau$ and the terms of the simply typed lambda calculus with pairs $(t, u)$ and the destructor $\mathsf{let}\ (x, y) = t\ \mathsf{in}\ u$. A context $\Gamma$ is a finite list of distinct typed variables, and $\Gamma, \Delta$ denotes the union of two contexts with no common variable. The linear type system is the least relation $\Gamma \vdash t : \tau$ closed under these rules.

1. Variable: $x : \tau \vdash x : \tau$, with exactly one variable in the context.
2. Abstraction: if $\Gamma, x : \sigma \vdash t : \tau$, then $\Gamma \vdash \lambda x.\, t : \sigma \multimap \tau$.
3. Application: if $\Gamma \vdash t : \sigma \multimap \tau$ and $\Delta \vdash u : \sigma$, then $\Gamma, \Delta \vdash t\, u : \tau$.
4. Pairing: if $\Gamma \vdash t : \sigma$ and $\Delta \vdash u : \tau$, then $\Gamma, \Delta \vdash (t, u) : \sigma \otimes \tau$.
5. Unpairing: if $\Gamma \vdash t : \sigma \otimes \rho$ and $\Delta, x : \sigma, y : \rho \vdash u : \tau$, then $\Gamma, \Delta \vdash \mathsf{let}\ (x, y) = t\ \mathsf{in}\ u : \tau$.
6. Exchange: the order of variables in a context does not matter.

The context is split between subterms, and the variable rule allows no extra variables. So every variable of $\Gamma$ occurs exactly once in $t$ whenever $\Gamma \vdash t : \tau$.