{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:13:17Z","timestamp":1725487997491},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730002"},{"type":"electronic","value":"9783540730019"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73001-9_41","type":"book-chapter","created":{"date-parts":[[2007,7,24]],"date-time":"2007-07-24T11:16:31Z","timestamp":1185275791000},"page":"398-407","source":"Crossref","is-referenced-by-count":1,"title":["Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus"],"prefix":"10.1007","author":[{"given":"Kentaro","family":"Kikuchi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"41_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1016\/S0304-3975(97)00183-7","volume":"211","author":"R. Bloo","year":"1999","unstructured":"Bloo, R., Geuvers, H.: Explicit substitution: On the edge of strong normalization. Theoretical Computer Science\u00a0211, 375\u2013395 (1999)","journal-title":"Theoretical Computer Science"},{"key":"41_CR2","doi-asserted-by":"publisher","first-page":"755","DOI":"10.2307\/2275572","volume":"62","author":"V. Danos","year":"1997","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: A new deconstructive logic: Linear logic. The Journal of Symbolic Logic\u00a062, 755\u2013807 (1997)","journal-title":"The Journal of Symbolic Logic"},{"key":"41_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/3-540-45022-X_51","volume-title":"Automata, Languages and Programming","author":"J. Esp\u00edrito Santo","year":"2000","unstructured":"Esp\u00edrito Santo, J.: Revisiting the correspondence between cut elimination and normalisation. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 600\u2013611. Springer, Heidelberg (2000)"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schliessen. Mathematische Zeitschrift, 39: pp. 176\u2013210, pp. 405\u2013431, English translation in [9 pp. 68\u2013131] (1935)","DOI":"10.1007\/BF01201363"},{"key":"41_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"key":"41_CR6","unstructured":"Hardin, T.: R\u00e9sultats de confluence pour les r\u00e8gles fortes de la logique combinatoire cat\u00e9gorique et liens avec les lambda-calculs. Th\u00e8se de doctorat, Universit\u00e9 de Paris VII (1987)"},{"key":"41_CR7","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pp. 479\u2013490. Academic Press, San Diego (1980)"},{"key":"41_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/11916277_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Kikuchi","year":"2006","unstructured":"Kikuchi, K.: On a local-step cut-elimination procedure for the intuitionistic sequent calculus. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 120\u2013134. Springer, Heidelberg (2006)"},{"volume-title":"The Collected Papers of Gerhard Gentzen","year":"1969","key":"41_CR9","unstructured":"Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam (1969)"},{"key":"41_CR10","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M. Takahashi","year":"1995","unstructured":"Takahashi, M.: Parallel reductions in \u03bb-calculus. Information and Computation\u00a0118, 120\u2013127 (1995)","journal-title":"Information and Computation"},{"key":"41_CR11","first-page":"123","volume":"45","author":"C. Urban","year":"2001","unstructured":"Urban, C., Bierman, G.M.: Strong normalisation of cut-elimination in classical logic. Fundamenta Informaticae\u00a045, 123\u2013155 (2001)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Computation and Logic in the Real World"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73001-9_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T08:18:16Z","timestamp":1556698696000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73001-9_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540730002","9783540730019"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73001-9_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}