Continuation Semantics

Origin. Barker, Shan (2006+). Continuations from PL. Scope-taking unified. Tower notation. Foundation of continuation-based NL semantics.

Models. Meanings as continuation transformers. Scope-taking via continuations. Tower types. Unified treatment of quantifiers, focus, binding. Programming language connection.

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.

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

Symbols.

Symbol	Unicode	Meaning
k	—	continuation
(α→r)→r	—	continuation type
tower	—	tower notation
reset, shift	—	control operators

Metatheory. Continuations. Scope as evaluation order. Tower types. Unification.

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

Limitations. Complexity. Learning curve. Implementation. Non-standard types.