{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T17:49:01Z","timestamp":1791049741045,"version":"4.1.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2007,10,24]],"date-time":"2007-10-24T00:00:00Z","timestamp":1193184000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2007,11,20]]},"DOI":"10.1007\/s10990-007-9007-z","type":"journal-article","created":{"date-parts":[[2007,10,23]],"date-time":"2007-10-23T16:11:28Z","timestamp":1193155888000},"page":"403-429","source":"Crossref","is-referenced-by-count":15,"title":["A proof-theoretic foundation of abortive continuations"],"prefix":"10.1007","volume":"20","author":[{"given":"Zena M.","family":"Ariola","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hugo","family":"Herbelin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amr","family":"Sabry","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,10,24]]},"reference":[{"key":"9007_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"871","DOI":"10.1007\/3-540-45061-0_68","volume-title":"Thirtieth International Colloquium on Automata, Languages and Programming, ICALP\u201903, Eindhoven, The Netherlands, June 30\u2013July 4, 2003","author":"Z.M. Ariola","year":"2003","unstructured":"Ariola, Z.M., Herbelin, H.: Minimal classical logic and control operators. In: Thirtieth International Colloquium on Automata, Languages and Programming, ICALP\u201903, Eindhoven, The Netherlands, June 30\u2013July 4, 2003. Lecture Notes in Computer Science, vol.\u00a02719, pp.\u00a0871\u2013885. Springer, New York (2003)"},{"key":"9007_CR2","first-page":"40","volume-title":"ACM SIGPLAN International Conference on Functional Programming","author":"Z.M. Ariola","year":"2004","unstructured":"Ariola, Z.M., Herbelin, H., Sabry, A.: A type-theoretic foundation of continuations and prompts. In: ACM SIGPLAN International Conference on Functional Programming, pp.\u00a040\u201353. ACM Press, New York (2004)"},{"key":"9007_CR3","unstructured":"Ariola, Z.M., Herbelin, H., Sabry, A.: A proof-theoretic foundation of abortive continuations (extended version). Technical Report TR608, Computer Science Department, Indiana University (2005)"},{"issue":"1","key":"9007_CR4","doi-asserted-by":"crossref","first-page":"276","DOI":"10.2307\/2274919","volume":"56","author":"A. Avron","year":"1991","unstructured":"Avron, A.: Natural 3-valued logics\u2014characterization and proof theory. J. Symb. Log. 56(1), 276\u2013294 (1991)","journal-title":"J. Symb. Log."},{"key":"9007_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/BFb0037097","volume-title":"Proceedings 1st Intl. Conf. on Typed Lambda Calculi and Applications, TLCA\u201993, Utrecht, The Netherlands, 16\u201318 March 1993","author":"F. Barbanera","year":"1993","unstructured":"Barbanera, F., Berardi, S.: Extracting constructive content from classical logic via control-like reductions. In: Bezem, M., Groote, J.F. (eds.) Proceedings 1st Intl. Conf. on Typed Lambda Calculi and Applications, TLCA\u201993, Utrecht, The Netherlands, 16\u201318 March 1993. Lecture Notes in Computer Science, vol.\u00a0664, pp.\u00a045\u201359. Springer, Berlin (1993)"},{"key":"9007_CR6","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"H.P. Barendregt","year":"1992","unstructured":"Barendregt, H.P.: Lambda calculi with types. In: Maibaum, A.G. (ed.) Handbook of Logic in Computer Science, vol.\u00a02, pp.\u00a0117\u2013309. Oxford University Press, Oxford (1992)"},{"key":"9007_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/BFb0055783","volume-title":"Mathematical Foundations of Computer Science","author":"G. Bierman","year":"1998","unstructured":"Bierman, G.: A computational interpretation of the lambda-mu calculus. In: Brim, L., Gruska, J., Zlatuska, J. (eds.) Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol.\u00a01450, pp.\u00a0336\u2013345. Springer, New York (1998)"},{"issue":"6","key":"9007_CR8","doi-asserted-by":"crossref","first-page":"625","DOI":"10.1017\/S0956796899003512","volume":"9","author":"T. Crolard","year":"1999","unstructured":"Crolard, T.: A confluent lambda-calculus with a catch\/throw mechanism. J. Funct. Program. 9(6), 625\u2013647 (1999)","journal-title":"J. Funct. Program."},{"key":"9007_CR9","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-58216-9_27","volume-title":"Logic Programming and Automated Reasoning, Proc. of the 5th International Conference, LPAR\u201994","author":"P. Groote de","year":"1994","unstructured":"de Groote, P.: On the relation between the lambda-mu calculus and the syntactic theory of sequential control. In: Pfennig, F. (ed.) Logic Programming and Automated Reasoning, Proc. of the 5th International Conference, LPAR\u201994, pp.\u00a031\u201343. Springer, Berlin (1994)"},{"issue":"6","key":"9007_CR10","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1017\/S0960129598002667","volume":"8","author":"P. Groote de","year":"1998","unstructured":"de Groote, P.: An environment machine for the lambda-mu-calculus. Math. Struct. Comput. Sci. 8(6), 637\u2013669 (1998)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9007_CR11","first-page":"180","volume-title":"Proceedings of the 15th ACM Symposium on Principles of Programming Languages (POPL\u201988)","author":"M. Felleisen","year":"1988","unstructured":"Felleisen, M.: The theory and practice of first-class prompts. In: Proceedings of the 15th ACM Symposium on Principles of Programming Languages (POPL\u201988), pp.\u00a0180\u2013190. ACM Press, New York (1988)"},{"key":"9007_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-52592-0_60","volume-title":"ESOP\u201990 3rd European Symposium on Programming, Copenhagen, Denmark","author":"M. Felleisen","year":"1990","unstructured":"Felleisen, M.: On the expressive power of programming languages. In: Jones, N. (ed.) ESOP\u201990 3rd European Symposium on Programming, Copenhagen, Denmark. Lecture Notes in Computer Science, vol.\u00a0432, pp.\u00a0134\u2013151. Springer, New York (1990)"},{"issue":"2","key":"9007_CR13","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M. Felleisen","year":"1992","unstructured":"Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235\u2013271 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"9007_CR14","first-page":"68","volume-title":"Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M. (ed.) Collected Papers of Gerhard Gentzen, pp.\u00a068\u2013131. North-Holland, Amsterdam (1969)"},{"issue":"3","key":"9007_CR15","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.-Y. Girard","year":"1991","unstructured":"Girard, J.-Y.: A new constructive logic: classical logic. Math. Struct. Comput. Sci. 1(3), 255\u2013296 (1991)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9007_CR16","volume-title":"Proof Theory and Automated Deduction","author":"J. Goubault-Larrecq","year":"2001","unstructured":"Goubault-Larrecq, J., Mackie, I.: Proof Theory and Automated Deduction. Kluwer Academic, Dordrecht (2001)"},{"key":"9007_CR17","first-page":"47","volume-title":"Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL\u201990, San Francisco, CA, USA, 17\u201319 Jan. 1990","author":"T.G. Griffin","year":"1990","unstructured":"Griffin, T.G.: The formulae-as-types notion of control. In: Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL\u201990, San Francisco, CA, USA, 17\u201319 Jan. 1990, pp.\u00a047\u201357. ACM Press, New York (1990)"},{"issue":"4","key":"9007_CR18","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1017\/S0960129500001195","volume":"5","author":"M. Hofmann","year":"1995","unstructured":"Hofmann, M.: Sound and complete axiomatisations of call-by-balue control operators. Math. Struct. Comput. Sci. 5(4), 461\u2013482 (1995)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9007_CR19","first-page":"119","volume":"4","author":"I. Johansson","year":"1937","unstructured":"Johansson, I.: Der Minimalkalk\u00fcl, ein reduzierter intuitionistischer Formalismus. Compos. Math. 4, 119\u2013136 (1937)","journal-title":"Compos. Math."},{"key":"9007_CR20","series-title":"SIGPLAN Notices","first-page":"177","volume-title":"Proc. of 8th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP\u201903, Uppsala, Sweden, 25\u201329 Aug. 2003","author":"Y. Kameyama","year":"2003","unstructured":"Kameyama, Y., Hasegawa, M.: A sound and complete axiomatization of delimited continuations. In: Proc. of 8th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP\u201903, Uppsala, Sweden, 25\u201329 Aug. 2003. SIGPLAN Notices, vol.\u00a038(9), pp.\u00a0177\u2013188. ACM Press, New York (2003)"},{"key":"9007_CR21","volume-title":"Computation as Logic","author":"R. Lalement","year":"1993","unstructured":"Lalement, R.: Computation as Logic. Prentice Hall International Series in Computer Science, Amsterdam (1993)"},{"key":"9007_CR22","first-page":"215","volume-title":"Conf. Record 24th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL\u201997, Paris, France, 15\u201317 Jan. 1997","author":"C.-H.L. Ong","year":"1997","unstructured":"Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: Conf. Record 24th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL\u201997, Paris, France, 15\u201317 Jan. 1997, pp.\u00a0215\u2013227. ACM Press, New York (1997)"},{"key":"9007_CR23","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning: International Conference LPAR\u201992 Proceedings, St. Petersburg, Russia","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: Lambda-mu-calculus: an algorithmic interpretation of classical natural deduction. In: Logic Programming and Automated Reasoning: International Conference LPAR\u201992 Proceedings, St. Petersburg, Russia, pp.\u00a0190\u2013201. Springer, New York (1992)"},{"key":"9007_CR24","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/BFb0022575","volume":"713","author":"M. Parigot","year":"1993","unstructured":"Parigot, M.: Classical proofs as programs. Comput. Log. Theory 713, 263\u2013276 (1993)","journal-title":"Comput. Log. Theory"},{"key":"9007_CR25","doi-asserted-by":"crossref","unstructured":"Parigot, M.: Strong normalization for second order classical natural deduction. In: Proceedings 8th Annual IEEE Symp. on Logic in Computer Science, LICS\u201993, pp.\u00a039\u201347. IEEE Computer Society Press (1993)","DOI":"10.1109\/LICS.1993.287602"},{"issue":"4","key":"9007_CR26","doi-asserted-by":"crossref","first-page":"1461","DOI":"10.2307\/2275652","volume":"62","author":"M. Parigot","year":"1997","unstructured":"Parigot, M.: Proofs of strong normalisation for second order classical natural deduction. J. Symb. Log. 62(4), 1461\u20131479 (1997)","journal-title":"J. Symb. Log."},{"key":"9007_CR27","volume-title":"Natural Deduction, a Proof-Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction, a Proof-Theoretical Study. Almquist and Wiksell, Stockholm (1965)"},{"key":"9007_CR28","unstructured":"Py, W.: Confluence en \u03bb \u03bc-calcul. Ph.D. thesis, Universit\u00e9 de Savoie (1998)"},{"issue":"3\u20134","key":"9007_CR29","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BF01019462","volume":"6","author":"A. Sabry","year":"1993","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp Symb. Comput. 6(3\u20134), 289\u2013360 (1993)","journal-title":"Lisp Symb. Comput."},{"issue":"2","key":"9007_CR30","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1017\/S096012950000311X","volume":"11","author":"P. Selinger","year":"2001","unstructured":"Selinger, P.: Control categories and duality: on the categorical semantics of the lambda-mu calculus. Math. Struct. Comput. Sci. 11(2), 207\u2013260 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"6","key":"9007_CR31","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1017\/S0956796898003141","volume":"8","author":"T. Streicher","year":"1998","unstructured":"Streicher, T., Reus, B.: Classical logic: continuation semantics and abstract machines. J. Funct. Program. 8(6), 543\u2013572 (1998)","journal-title":"J. Funct. Program."},{"key":"9007_CR32","volume-title":"Logic and Structure","author":"D. Dalen van","year":"1997","unstructured":"van Dalen, D.: Logic and Structure. Springer, New York (1997)"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9007-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-007-9007-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9007-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T01:29:41Z","timestamp":1559352581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-007-9007-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,24]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,11,20]]}},"alternative-id":["9007"],"URL":"https:\/\/doi.org\/10.1007\/s10990-007-9007-z","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10,24]]}}}