{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:14:08Z","timestamp":1759637648945},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540653882"},{"type":"electronic","value":"9783540493662"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49366-2_5","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T18:48:47Z","timestamp":1194979727000},"page":"61-78","source":"Crossref","is-referenced-by-count":3,"title":["Cut Elimination for Classical Proofs as Continuation Passing Style Computation"],"prefix":"10.1007","author":[{"given":"Ichiro","family":"Ogata","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1998,11,30]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi, Luca Cardelli, P.-L. Curien, and Jean-Jacques L\u00e9vy. Explicit substitutions. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 31\u201346, San Francisco, California, January 1990.","DOI":"10.1145\/96709.96712"},{"key":"5_CR2","unstructured":"Vincent Danos. La Logique Lin\u00e9aire Appliqu\u00e9e \u00e0 l'\u00e9tude de Divers Processus de Normalisation (Principalement du \u03bb-Calcul). PhD thesis, University of Paris VII, June 1990."},{"key":"5_CR3","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. Proceedings of the Workshop on Linear Logic, Ithaca, New York, June 1993.","DOI":"10.1017\/CBO9780511629150.011"},{"key":"5_CR4","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":"5_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0017475","volume-title":"Proceedings Trees in Algebra and Programming-CAAP\u201994","author":"P. Groote de","year":"1994","unstructured":"Phillipe deGroote. A cps-translation of the \u03bb\u03bc-calculus. In Proceedings Trees in Algebra and Programming-CAAP\u201994, pages 85\u201399. Springer-Verlag LNCS 787, April 1994."},{"key":"5_CR6","unstructured":"Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, and Bruce Duba. Reasoning with continuations. In Proceedings, Symposium on Logic in Computer Science, pages 131\u2013141, Cambridge, Massachusetts, 16\u201318 June 1986. IEEE Computer Society."},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische schlie\u00dfen. Mathematische Zeitschrift, 39:176\u2013210, 405\u2013431, 1935.","journal-title":"Mathematische Zeitschrift"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1\u2013102, 1987.","journal-title":"Theoretical Computer Science"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.-Y. Girard","year":"1991","unstructured":"Jean-Yves Girard. A new constructive logic: Classical logic. Mathematical Structures in Computer Science, 1:255\u2013296, 1991.","journal-title":"Mathematical Structures in Computer Science"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","volume":"59","author":"J.-Y. Girard","year":"1993","unstructured":"Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201\u2013217, 1993.","journal-title":"Annals of Pure and Applied Logic"},{"key":"5_CR11","unstructured":"Jean-Yves Girard, Yves Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1988."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Timothy G. Griffin. A formulae-as-types notion of control. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 47\u201358, San Francisco, California, January 1990.","DOI":"10.1145\/96709.96714"},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","first-page":"933","volume-title":"Proceedings of the 1994 Annual Conference of the European Association for Computer Science Logic","author":"H. Herbelin","year":"1994","unstructured":"Hugo Herbelin. A \u03bb-calculus structure ismorphic to gentzen-style sequent calculus structure. In L. Pacholski and J. Tiuryn, editors, Proceedings of the 1994 Annual Conference of the European Association for Computer Science Logic, Kazimierz, Poland, September 1994. Springer Verlag, LNCS 933."},{"key":"5_CR14","unstructured":"Grigori Mints. Normal forms for sequent derivations. In Piergiorgio Odifreddi, editor, Kreiseliana-About and Around George Kreisel. A K Peters Ltd., March 1996."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Chetan R. Murthy. A computational analysis of Girard\u2019s translation and LC. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 90\u2013101, Santa Cruz, California, 22\u201325 June 1992. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1992.185523"},{"key":"5_CR16","unstructured":"Ichiro Ogata. Classical proofs as programs, cut elimination as computation. Manuscript, June 1998."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"C.-H. L. Ong and C. A. Stewart. A curry-howard foundation for functional computation with control. In Proceedings of ACM SIGPLAN-SIGACT Symposium on Principle of Programming Languages, Paris, January 1997. ACM Press, 1997.","DOI":"10.1145\/263699.263722"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Michel Parigot. Free deduction: An analysis of \u201ccomputations\u201d in classical logic. In RCLP 1990\/1991, pages 361\u2013380, 1991.","DOI":"10.1007\/3-540-55460-2_27"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Michel Parigot. Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In LPAR 1992, pages 190\u2013201, 1992.","DOI":"10.1007\/BFb0013061"},{"key":"5_CR20","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."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Michel Parigot. Strong normalization for second order classical natural deduction. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 39\u201346, Montreal, Canada, 19\u201323 June 1993. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1993.287602"},{"issue":"2","key":"5_CR22","doi-asserted-by":"crossref","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 \u03bb-calculus. Theoretical Computer Science, 1(2):125\u2013159, December 1975.","journal-title":"Theoretical Computer Science"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/S0003-4843(77)80004-1","volume":"12","author":"G. Pottinger","year":"1977","unstructured":"G. Pottinger. Normalization as a homomorphic image of cut-elimination. Annals of Mathematical Logic, 12:323\u2013357, 1977.","journal-title":"Annals of Mathematical Logic"},{"key":"5_CR24","volume-title":"Natural Deduction, a Poof-Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz. Natural Deduction, a Poof-Theoretical Study. Almquist and Wiksell, Stockholm, 1965."},{"key":"5_CR25","series-title":"CSLI Lecture Notes","volume-title":"Lectures on Linear Logic","author":"A. S. Troelstra","year":"1992","unstructured":"Anne S. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992."},{"key":"5_CR26","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 ASIAN 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49366-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T10:16:56Z","timestamp":1556965016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49366-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540653882","9783540493662"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-49366-2_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}