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.

翻译：本文简要探讨逻辑与计算之间的关系。具体而言，本文研究了直觉主义命题逻辑在基扩展语义学这一证明论语义学形式中的完备性证明，与计算理论中被称为续延传递语义的基本思想之间的关联。我们分别从自然演绎和λ演算中的归约以及证明搜索的角度阐释了后者。通过分析Sandqvist的完备性定理证明（从Kripke和Heyting语义学的数学视角审视），探讨了完备性与续延之间的关系。我们的分析揭示出，续延的句法表示如何体现了关于意义与使用之间关系的内涵语义直觉。借助证明论语义学的工具，这些直觉得到了精确表述。