{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:48:22Z","timestamp":1762458502200},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540368342"},{"type":"electronic","value":"9783540368359"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11805618_15","type":"book-chapter","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T10:29:13Z","timestamp":1153823353000},"page":"197-211","source":"Crossref","is-referenced-by-count":3,"title":["Structural Proof Theory as Rewriting"],"prefix":"10.1007","author":[{"given":"J. Esp\u00edrito","family":"Santo","sequence":"first","affiliation":[]},{"given":"M. J.","family":"Frade","sequence":"additional","affiliation":[]},{"given":"L.","family":"Pinto","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/A:1005099619660","volume":"60","author":"R. Dyckhoff","year":"1998","unstructured":"Dyckhoff, R., Pinto, L.: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic. Studia Logica\u00a060, 107\u2013118 (1998)","journal-title":"Studia Logica"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/S0304-3975(98)00138-8","volume":"212","author":"R. Dyckhoff","year":"1999","unstructured":"Dyckhoff, R., Pinto, L.: Permutability of proofs in intuitionistic sequent calculi. Theoretical Computer Science\u00a0212, 141\u2013155 (1999)","journal-title":"Theoretical Computer Science"},{"unstructured":"Esp\u00edrito Santo, J.: Conservative extensions of the \u03bb-calculus for the computational interpretation of sequent calculus. PhD thesis, University of Edinburgh (2002), available at: \n                    \n                      http:\/\/www.lfcs.informatics.ed.ac.uk\/reports\/","key":"15_CR3"},{"key":"15_CR4","series-title":"Lecture Notes in Artificial Intelligence","first-page":"354","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Esp\u00edrito Santo","year":"2002","unstructured":"Esp\u00edrito Santo, J.: An isomorphism between a fragment of sequent calculus and an extension of natural deduction. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 354\u2013366. Springer, Heidelberg (2002)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/3-540-44904-3_20","volume-title":"Typed Lambda Calculi and Applications","author":"J.E. Santo","year":"2003","unstructured":"Santo, J.E., Pinto, L.: Permutative conversions in intuitionistic multiary sequent calculus with cuts. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 286\u2013300. Springer, Heidelberg (2003)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-540-24849-1_13","volume-title":"Types for Proofs and Programs","author":"J.E. Santo","year":"2004","unstructured":"Santo, J.E., Pinto, L.: Confluence and strong normalisation of the generalised multiary \u03bb-calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 194\u2013209. Springer, Heidelberg (2004)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0022247","volume-title":"Computer Science Logic","author":"H. Herbelin","year":"1995","unstructured":"Herbelin, H.: A \u03bb-calculus structure isomorphic to a Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, pp. 61\u201375. Springer, Heidelberg (1995)"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s00153-002-0156-9","volume":"42","author":"F. Joachimski","year":"2003","unstructured":"Joachimski, F., Matthes, R.: Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and G\u00f6del\u2019s T. Archive for Mathematical Logic\u00a042, 59\u201387 (2003)","journal-title":"Archive for Mathematical Logic"},{"key":"15_CR9","first-page":"469","volume-title":"Kreiseliana","author":"G. Mints","year":"1996","unstructured":"Mints, G.: Normal forms for sequent derivations. In: Odifreddi, P. (ed.) Kreiseliana, pp. 469\u2013492. A. K. Peters, Wellesley, Massachusetts (1996)"},{"doi-asserted-by":"crossref","unstructured":"Negri, S., von Plato, J.: Structural Proof Theory, Cambridge (2001)","key":"15_CR10","DOI":"10.1017\/CBO9780511527340"},{"unstructured":"Rose, K.: Explicit substitutions: Tutorial & survey. Technical Report LS-96-3, BRICS (1996)","key":"15_CR11"},{"doi-asserted-by":"crossref","unstructured":"Schwichtenberg, H.: Termination of permutative conversions in intuitionistic gentzen calculi. Theoretical Computer Science\u00a0212 (1999)","key":"15_CR12","DOI":"10.1016\/S0304-3975(98)00143-1"},{"issue":"7","key":"15_CR13","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001530100091","volume":"40","author":"J. Plato von","year":"2001","unstructured":"von Plato, J.: Natural deduction with general elimination rules. Annals of Mathematical Logic\u00a040(7), 541\u2013567 (2001)","journal-title":"Annals of Mathematical Logic"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11805618_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:25:59Z","timestamp":1619493959000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11805618_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540368342","9783540368359"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11805618_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}