**Abstract:**
The `Glue Semantics' used in Lexical Functional Grammar is formulated as
linear logic proofs labeled with a combination of linear and non-linear typed
lambda-calculus (linear structure determined by the proof, non-linear for
expressing the actual meanings). The labeling looks superficially as if it
might be somewhat arbitrary, but I will here show that this is not necessarily
the case, if the semantic interpretations inhabit a Cartesian Closed Category
(CCC). This is because a glue proof can be identified with a `balanced
sequent' of the implication-tensor fragment of intuitionistic linear logic (a
sequent in which each literal appears at most twice), which is therefore a
balanced sequent of intuitionistic implication-conjunction logic, which a
theorem proved by Babaev and Solovev in 1982 shows has at most one normal
proof. A closed cartesian functor can then produce the semantic
interpretation from this proof. The functor can furthermore be factored
through a number of other CCCs produced naturally by the glue proof, which are
shown to have possible useful empirical properties for linguistics.

**Changes from V1:** Typoes, expository improvements and some
additional content.