 Let us start with the Curry-Howard correspondence for LP. The choice of LP as the calculus of natural language semantics captures the fact that meaning composition is a resource-sensitive process: in interpreting a derivation, no material can be copied or thrown away. Let us refer to the terms of the simply typed linear lambda calculus as Λ(Lin).  In the absence of Contraction and Weakening, this is the smallest set such that, given a denumerably infinite set of variables Var,