Hofmann, Martin Sound and complete axiomatisations of call-by-value control operators. (English) Zbl 0846.68066 Math. Struct. Comput. Sci. 5, No. 4, 461-482 (1995). 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. Cited in 9 Documents 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 Keywords:call-by-value \(\lambda\)-calculus; propositional logic PDFBibTeX XMLCite \textit{M. Hofmann}, Math. Struct. Comput. Sci. 5, No. 4, 461--482 (1995; Zbl 0846.68066) 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.