{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:34:46Z","timestamp":1725496486263},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540668565"},{"type":"electronic","value":"9783540466741"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46674-6_23","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T10:50:17Z","timestamp":1196333417000},"page":"266-280","source":"Crossref","is-referenced-by-count":2,"title":["A CPS-Transform of Constructive Classical Logic"],"prefix":"10.1007","author":[{"given":"Ichiro","family":"Ogata","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,11,19]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. Sequent calculi for second order logic. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 211\u2013224. Cambridge University Press, 1995.","DOI":"10.1017\/CBO9780511629150.011"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. A new deconstructive logic: linear logic. Journal of Symbolic Logic, 62(3), September 1997.","DOI":"10.2307\/2275572"},{"key":"23_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/BFb0017475","volume-title":"Proc. CAAP\u201994","author":"P. Groote de","year":"1994","unstructured":"Phillipe de Groote. A cps-translation of the-calculus. In Proc. CAAP\u201994, pages 85\u201399. Springer-Verlag LNCS 787, April 1994."},{"key":"23_CR4","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BF01201363","volume":"39176-210","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische schlie\u00dfen. Mathematische Zeitschrift, 39:176-210,405\u2013431, 1935.","journal-title":"Mathematische Zeitschrift"},{"key":"23_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CSL\u2019 94","author":"H. Herbelin","year":"1994","unstructured":"Hugo Herbelin. A _-calculus structure ismorphic to gentzen-style sequent calculus structure. In Proc. CSL\u2019 94, Kazimierz, Poland, September 1994. Springer Verlag, LNCS 933."},{"key":"23_CR6","unstructured":"Martin Hofmann and Thomas Streicher. Continuation models are universal for __-calculus. In Proc. LICS\u2019 97, june 1997."},{"key":"23_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/3-540-49366-2_5","volume-title":"Proc.Asian\u201998","author":"I. Ogata","year":"1998","unstructured":"Ichiro Ogata. Cut elimination for classical proofs as continuation passing style computation. In Proc.Asian\u201998, pages 61\u201378, Manila, Philippines, December 1998. Springer-Verlag LNCS 1538."},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Ichiro Ogata. Constructive classical logic as cps-calculus. To appear in International Journal of Foundations of computer science, 1999.","DOI":"10.1007\/3-540-46674-6_23"},{"key":"23_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/BFb0022575","volume-title":"3rd Kurt G\u00f6del Colloquium","author":"M. Parigot","year":"1993","unstructured":"Michel Parigot. Classical proofs as programs. In 3rd Kurt G\u00f6del Colloquium, pages 263\u2013276. Springer-Verlag LNCS 713, 1993."},{"issue":"2","key":"23_CR10","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. D. Plotkin","year":"1975","unstructured":"G. D. Plotkin. Call-by-name, call-by-value and the _-calculus. Theoretical Computer Science, 1(2):125\u2013159, December 1975.","journal-title":"Theoretical Computer Science"},{"key":"23_CR11","unstructured":"Peter Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Presented at MFPS\u2019 98, London, 1999."},{"key":"23_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0003-4843(74)90010-2","volume":"7","author":"J. I. Zucker","year":"1974","unstructured":"J. I. Zucker. Correspondence between cut-elimination and normalization, part i and ii. Annals of Mathematical Logic, 7:1\u2013156, 1974.","journal-title":"Annals of Mathematical Logic"}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN\u201999"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46674-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T04:56:34Z","timestamp":1557032194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46674-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668565","9783540466741"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-46674-6_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}