{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T11:17:11Z","timestamp":1778757431316,"version":"3.51.4"},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":4842,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1995,12]]},"abstract":"<jats:p>We formulate a typed version of call-by-value \u03bb-calculus containing variants of Felleisen's control operators <jats:italic>A<\/jats:italic> and <jats:italic>C<\/jats:italic> 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.<\/jats:p>","DOI":"10.1017\/s0960129500001195","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:00:09Z","timestamp":1236157209000},"page":"461-482","source":"Crossref","is-referenced-by-count":21,"title":["Sound and complete axiomatisations of call-by-value control operators"],"prefix":"10.1017","volume":"5","author":[{"given":"Martin","family":"Hofmann","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500001195_ref016","article-title":"A theory for program and data specification","volume":"10","author":"Talcott","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"S0960129500001195_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"S0960129500001195_ref005","unstructured":"Filinski A. (1989) Declarative Comtinuations and Categorical Duality, Master's thesis, Computer Science Department, University of Copenhagen, DIKU Report 89\/11."},{"key":"S0960129500001195_ref002","volume-title":"Compiling with Continuations","author":"Appel","year":"1992"},{"key":"S0960129500001195_ref011","unstructured":"Murthy C. (1991) An evaluation semantics for classical proofs. In: Proceedings of the sixth IEEE Symposium on Logic in Computer Science (LICS)."},{"key":"S0960129500001195_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90109-5"},{"key":"S0960129500001195_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0960129500001195_ref006","doi-asserted-by":"crossref","unstructured":"Griffin T. (1990) A formulae-as-types notion of control. In: Proc. 17th ACM Symposium on Principles of Programming Languages 47\u201358.","DOI":"10.1145\/96709.96714"},{"key":"S0960129500001195_ref001","unstructured":"Agapiev B. and Moggi E. (1991) Declarative Continuations and Monads. (Unpublished draft)"},{"key":"S0960129500001195_ref003","volume-title":"Category Theory for Computing Science","author":"Barr","year":"1990"},{"key":"S0960129500001195_ref007","unstructured":"Jacobs B. (1991) Categorical Type Theory, PhD thesis, University of Nijmegen."},{"key":"S0960129500001195_ref009","volume-title":"Introduction to Higher-Order Categorical Logic","author":"Lambek","year":"1985"},{"key":"S0960129500001195_ref008","unstructured":"Krivine J.-L. (Unpublished note) Classical Logic, Storage Operators, and Second Order Lambda-Calculus."},{"key":"S0960129500001195_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129500001195_ref013","doi-asserted-by":"publisher","DOI":"10.1145\/15042.15043"},{"key":"S0960129500001195_ref014","doi-asserted-by":"crossref","unstructured":"Reynolds J. C. (1972) Definitional interpreters for higher-order programming languages. In: Proceedings of the 25th ACM National Conference 717\u2013740.","DOI":"10.1145\/800194.805852"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500001195","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T20:12:40Z","timestamp":1557778360000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500001195\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,12]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,12]]}},"alternative-id":["S0960129500001195"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500001195","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,12]]}}}