Continuations and Completeness in Proof-theoretic Semantics
For logicians and computer scientists interested in the foundations of proof-theoretic semantics, this paper provides a conceptual link between completeness proofs and continuations, but the contribution is primarily theoretical and incremental.
This paper explores the relationship between completeness in proof-theoretic semantics (base-extension semantics) for intuitionistic propositional logic and continuation-passing semantics from computation theory, analyzing Sandqvist's completeness proof through the lens of Kripke and Heyting semantics. It reveals how syntactic representations of continuations embody intensional semantical intuitions about meaning and use.
This is a short paper about the relationship between logic and computation. More specifically, it is about a relationship between the completeness proof for intuitionistic propositional logic within the form of proof-theoretic semantics that is known as base-extension semantics and a fundamental idea from the theory of computation called continuation-passing semantics. The latter is explained herein both in terms of reduction in natural deduction and the lambda calculus and in terms of proof-search. The relationship between completeness and continuations is explored through an analysis of Sandqvist's proof of the completeness theorem as seen from the mathematical perspective of Kripke's and Heyting's semantics. Our analysis can be seen to reveal how syntactic representations of continuations embody intensional semantical intuitions about the relationship between their meaning and use. These intuitions are made precise using the tools of proof-theoretic semantics.