Continuation Semantics

Origin. Continuations come from denotational semantics of programming languages — Strachey and Wadsworth, "Continuations: a mathematical semantics for handling full jumps" (1974), and Plotkin's CPS transform (1975). Philippe de Groote, "Type raising, continuations, and classical logic" (2001), brought them to Montague semantics; Chris Barker, "Continuations and the nature of quantification" (Natural Language Semantics 10, 2002), argued that quantification just is continuation-taking; Chung-chieh Shan's dissertation Linguistic Side Effects (Harvard, 2005) treated scope, focus, and interrogation as computational effects. Barker and Shan, "Explaining crossover and superiority as left-to-right evaluation" (Linguistics and Philosophy 29, 2006) and Continuations and Natural Language (Oxford, 2014), give the tower calculus.

Models. The continuation of an expression is what the rest of the derivation will do with its value. An expression that takes scope is one that does not simply hand a value up but instead receives the surrounding computation as an argument and decides what to do with it. Since Montague already assigned every noun phrase the type ⟨⟨e,t⟩,t⟩, which is exactly the continuation type over e, the observation is that PTQ's uniform type assignment is a continuation-passing transform performed by hand. Generalizing it makes scope-taking a property of the mode of composition rather than of a movement operation, and the same mechanism then covers focus, binding, and interrogatives.

Formalism.

Continuation: Continuation of α: what happens next with α's value. k: α → result. α feeds into k. Control abstraction.

Continuation type: (α → r) → r. Takes continuation, produces result. Quantifier type pattern. Scope-taking.

Quantifier as continuation: [[every student]]: (e → t) → t. λk.∀x[student(x) → k(x)]. Continuation k = scope. Takes scope, returns truth value.

Tower notation: β | γ ───── α α: at-issue meaning. β, γ: continuation levels. Multi-level.

Composition (tower): Continuation-passing style. Meanings compose through continuations. Scope emerges. No QR movement.

Scope ambiguity: "Someone loves everyone." Different evaluation orders. ∃ > ∀ or ∀ > ∃. Continuation order.

Type raising is the monadic unit: λx.λk.k(x) : e → (e → r) → r. Lifts a plain value into the continuation monad. "John" of type e becomes λk.k(j), Montague's λP.P(j). The PTQ type assignment is a CPS transform done by hand.

Lift and lower: Lift: a non-scope-taking word is raised to the tower level required by its neighbours. Lower: apply the completed tower to the identity continuation. Evaluation is finished by lowering, which is where the truth value appears.

Beyond quantifiers: Focus: continuation-based. Binding: same mechanism. Questions: scope-like. Unified analysis.

Delimited control (shift and reset): shift captures the current continuation; reset bounds how far it extends. Danvy and Filinski (1990) for the calculus. A reset boundary is a scope island: nothing takes scope past it.

Left-to-right evaluation: Arguments are evaluated in surface order. A binder must be evaluated before the pronoun it binds. Weak crossover and superiority follow from the order, not from a filter.

Symbols.

Metatheory. Type raising λx.λk.k(x) is the unit of the continuation monad, and the ⟨⟨e,t⟩,t⟩ type Montague assigns every noun phrase is the continuation type over e, so PTQ's uniform assignment is a continuation-passing transform carried out by hand. Under Curry–Howard the transform is the double-negation translation, and Griffin (1990) showed that control operators inhabit classically but not intuitionistically provable types — call/cc has the type of Peirce's law — so a scope-taking expression is a classical term. Barker (2002) showed that quantifier scope needs no movement operation once composition is continuized, and Barker and Shan (2006) derived weak crossover and superiority from a single assumption, left-to-right evaluation, in place of separate binding conditions. Scope islands are modelled by reset, the delimiter of Danvy and Filinski's (1990) shift/reset calculus. Shan (2002) and Charlow (2014) showed that the continuation monad subsumes Hamblin alternatives, which is what repairs the known incompatibility of pointwise composition with variable binding.

Applies to. Quantifier scope. Focus. Binding. Cross-categorial phenomena.

Limitations. The calculus overgenerates scope: once towers of arbitrary height are admitted, every permutation of scope-bearing elements is derivable, so island effects and clause-boundedness have to be imposed by placing reset delimiters that the syntax does not independently fix. Words have no single type — a lexical entry must be lifted to whatever level a derivation demands — so the lexicon specifies a schema rather than a denotation, and distinct derivations frequently deliver the same reading, giving spurious ambiguity that the system supplies no normal form to quotient away. The empirical case rests on linear order: crossover and superiority follow from left-to-right evaluation, but inverse scope is freely available, so order cannot be the only determinant. Everything the framework derives is also derivable by quantifier raising or type shifting, so its claim is unification, not coverage.

© 2026 Lingenic LLC