{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:15:54Z","timestamp":1725488154059},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540419600"},{"type":"electronic","value":"9783540454137"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45413-6_22","type":"book-chapter","created":{"date-parts":[[2007,8,4]],"date-time":"2007-08-04T08:51:43Z","timestamp":1186217503000},"page":"268-282","source":"Crossref","is-referenced-by-count":1,"title":["A Deconstruction of Non-deterministic Classical Cut Elimination"],"prefix":"10.1007","author":[{"given":"J.","family":"Laird","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,4,25]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"543","DOI":"10.2307\/2275407","volume":"59","author":"S. Abramsky","year":"1994","unstructured":"S. Abramsky, R. Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 59:543\u2013574, 1994.","journal-title":"Journal of Symbolic Logic"},{"key":"22_CR2","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0025","volume":"125","author":"F. Barbanera","year":"1996","unstructured":"F. Barbanera, and S. Berardi. A symmetric lambda calculus for classical program extraction. Information and Computation, 125:103\u2013117, 1996.","journal-title":"Information and Computation"},{"key":"22_CR3","unstructured":"H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics, revised edition. North-Holland, 1984."},{"key":"22_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0168-0072(92)90073-9","volume":"56","author":"A. Blass","year":"1992","unstructured":"A. Blass. A game semantics for linear logic. Annals of Pure and Applied logic, 56:183\u2013220, 1992.","journal-title":"Annals of Pure and Applied logic"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"325","DOI":"10.2307\/2275524","volume":"60","author":"T. Coquand","year":"1995","unstructured":"T. Coquand. A semantics of evidence for classical arithmetic. Journal of Symbolic Logic, 60:325\u2013337, 1995.","journal-title":"Journal of Symbolic Logic"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"T. Coquand. Computational content of classical logic. In A. Pitts and P. Dybjer, editor, Semantics and Logics of Computation. Cambridge University Press, 1997.","DOI":"10.1017\/CBO9780511526619.003"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"V. Danos, J.-B. Joinet and H. Schellinx. A new deconstructive logic, linear logic. Journal of Symbolic Logic, 62(3), 1996.","DOI":"10.2307\/2275572"},{"key":"22_CR8","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen. Unterschungen \u00fcber das logische Schlie\u00e9n I and II. Mathematische Zeitschrift, 39:176\u2013210, 405\u2013431, 1935.","journal-title":"Mathematische Zeitschrift"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Towards a geometry of interaction. In Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, 1989.","DOI":"10.1090\/conm\/092\/1003197"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.-Y. Girard","year":"1991","unstructured":"J.-Y. Girard. A new constructive logic: classical logic. Mathematical structures in Computer Science, 1:259\u2013256, 1991.","journal-title":"Mathematical structures in Computer Science"},{"key":"22_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","volume":"59","author":"J.-Y. Girard","year":"1993","unstructured":"J.-Y. 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":"22_CR12","unstructured":"J.-Y. Girard, P. Taylor and Y. Lafont. Proofs and Types. Cambridge University Press, 1990."},{"key":"22_CR13","unstructured":"K. G\u00f6del. On intuitionistic arithmetic and number theory. In M. Davis, editor, The undecidable, pages 75\u201381. Raven Press, 1965."},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"T. Griffin. A formulae-as-types notion of control. In Proc. ACM Conference on the Principles of Programming Languages, pages 47\u201358. ACM Press, 1990.","DOI":"10.1145\/96709.96714"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"M. Hennessey, and E. Ashcroft. Parameter passing and non-determinism. In Conference report of the ninth ACM Conference on Theory of Computing, pages 306\u2013311, 1977.","DOI":"10.1145\/800105.803420"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"M. Parigot. \u03bb\u03bc calculus: an algorithmic interpretation of classical natural deduction. In Proc. International Conference on Logic Programming and Automated Reasoning, pages 190\u2013201. Springer, 1992.","DOI":"10.1007\/BFb0013061"},{"key":"22_CR17","series-title":"Lect Notes Comput Sci","first-page":"356","volume-title":"Proceedings of TLCA `99","author":"C. Urban","year":"1999","unstructured":"C. Urban, and G. Bierman. Strong normalisation of cut-elimination in classical logic. In Proceedings of TLCA `99, number 1581 in LNCS, pages 356\u2013380. Springer, 1999."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45413-6_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:06:40Z","timestamp":1556737600000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45413-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540419600","9783540454137"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45413-6_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}