×

Sound and complete axiomatisations of call-by-value control operators. (English) Zbl 0846.68066

Summary: We formulate a typed version of call-by-value \(\lambda\)-calculus containing variants of Felleisen’s control operators \(\mathcal A\) and \(\mathcal C\) that provide explicit access to continuations and logically extend the propositions-as-types correspondence to classical propositional logic. We give an equational theory for this calculus, which is shown to be sound and complete with respect to a class of categorical models based on continuation-passing-style semantics.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
68N01 General topics in the theory of software
03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] DOI: 10.1016/0304-3975(87)90109-5 · Zbl 0643.03011 · doi:10.1016/0304-3975(87)90109-5
[2] Barr, Category Theory for Computing Science (1990) · Zbl 0714.18001
[3] Appel, Compiling with Continuations (1992)
[4] Talcott, Theoretical Computer Science 10 (1992)
[5] DOI: 10.1016/0890-5401(91)90052-4 · Zbl 0723.68073 · doi:10.1016/0890-5401(91)90052-4
[6] DOI: 10.1145/15042.15043 · doi:10.1145/15042.15043
[7] DOI: 10.1016/0304-3975(75)90017-1 · Zbl 0325.68006 · doi:10.1016/0304-3975(75)90017-1
[8] Lambek, Introduction to Higher-Order Categorical Logic (1985) · Zbl 0596.03002
[9] DOI: 10.1007/BF01019462 · doi:10.1007/BF01019462
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.