V2 of Paper as PDF:

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.