Continuations and Completeness in Proof-theoretic Semantics
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866918485981921280 |
|---|---|
| author | Gu, Tao Pym, David Ritter, Eike Robinson, Edmund |
| author_facet | Gu, Tao Pym, David Ritter, Eike Robinson, Edmund |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_04689 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Continuations and Completeness in Proof-theoretic Semantics Gu, Tao Pym, David Ritter, Eike Robinson, Edmund Logic Logic in Computer Science 03F07 (Primary) 03B20, 03B38, 18F10 (Secondary) F.4.1; F.3.3 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. |
| title | Continuations and Completeness in Proof-theoretic Semantics |
| topic | Logic Logic in Computer Science 03F07 (Primary) 03B20, 03B38, 18F10 (Secondary) F.4.1; F.3.3 |
| url | https://arxiv.org/abs/2605.04689 |