{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:25:26Z","timestamp":1748413526475},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2009,2,5]],"date-time":"2009-02-05T00:00:00Z","timestamp":1233792000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2009,11]]},"DOI":"10.1007\/s00224-009-9183-9","type":"journal-article","created":{"date-parts":[[2009,2,4]],"date-time":"2009-02-04T13:49:25Z","timestamp":1233755365000},"page":"963-994","source":"Crossref","is-referenced-by-count":9,"title":["The \u03bb-Calculus and the Unity of Structural Proof Theory"],"prefix":"10.1007","volume":"45","author":[{"given":"Jos\u00e9","family":"Esp\u00edrito Santo","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,2,5]]},"reference":[{"issue":"5","key":"9183_CR1","doi-asserted-by":"crossref","first-page":"639","DOI":"10.1093\/logcom\/13.5.639","volume":"13","author":"I. Cervesato","year":"2003","unstructured":"Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639\u2013688 (2003)","journal-title":"J. Log. Comput."},{"issue":"9","key":"9183_CR2","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/357766.351262","volume":"35","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. ACM SIGPLAN Not. 35(9), 233\u2013243 (2000). Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900), Montreal, Canada, September 18\u201321 (2000)","journal-title":"ACM SIGPLAN Not."},{"key":"9183_CR3","volume-title":"Combinatory Logic","author":"H.B. Curry","year":"1958","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic. Noth-Holland, Amsterdam (1958)"},{"key":"9183_CR4","doi-asserted-by":"crossref","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 Log. 60, 107\u2013118 (1998)","journal-title":"Studia Log."},{"key":"9183_CR5","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 212, 141\u2013155 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"9183_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1007\/3-540-45022-X_51","volume-title":"Proceedings of ICALP\u20192000","author":"J. Esp\u00edrito Santo","year":"2000","unstructured":"Esp\u00edrito Santo, J.: Revisiting the correspondence between cut-elimination and normalisation. In: Proceedings of ICALP\u20192000. Lecture Notes in Computer Science, vol. 1853, pp. 600\u2013611. Springer, Berlin (2000)"},{"key":"9183_CR7","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 http:\/\/www.lfcs.informatics.ed.ac.uk\/reports\/"},{"key":"9183_CR8","series-title":"Lecture Notes in Artificial Intelligence","first-page":"354","volume-title":"Proceedings of LPAR\u201902","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.) Proceedings of LPAR\u201902. Lecture Notes in Artificial Intelligence, vol. 2514, pp. 354\u2013366. Springer, Berlin (2002)"},{"key":"9183_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/978-3-540-73228-0_10","volume-title":"Proceedings of TLCA\u201907","author":"J. Esp\u00edrito Santo","year":"2007","unstructured":"Esp\u00edrito Santo, J.: Completing Herbelin\u2019s programme. In: Ronchi Della Rocca, S. (ed.) Proceedings of TLCA\u201907. Lecture Notes in Computer Science, vol. 4583, pp. 118\u2013132. Springer, Berlin (2007)"},{"key":"9183_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/978-3-540-73449-9_14","volume-title":"Proceedings of RTA\u201907","author":"J. Esp\u00edrito Santo","year":"2007","unstructured":"Esp\u00edrito Santo, J.: Delayed substitutions. In: Baader, F. (ed.) Proceedings of RTA\u201907. Lecture Notes in Computer Science, pp. 169\u2013183. Springer, Berlin (2007). (See also the manuscript, Addenda to \u2018Delayed Substitutions\u2019, available from the author\u2019s web page)"},{"key":"9183_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-540-73001-9_27","volume-title":"Proceedings of CiE\u201907","author":"J. Esp\u00edrito Santo","year":"2007","unstructured":"Esp\u00edrito Santo, J.: Refocusing generalised normalisation. In: Cooper, S.B., Lowe, B., Sorbi, A. (eds.) Proceedings of CiE\u201907. Lecture Notes in Computer Science, vol. 4497, pp. 258\u2013267. Springer, Berlin (2007)"},{"key":"9183_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/11805618_15","volume-title":"Proc. of RTA\u201906","author":"J. Esp\u00edrito Santo","year":"2006","unstructured":"Esp\u00edrito Santo, J., Frade, M.J., Pinto, L.: Structural proof theory as rewriting. In: Pfenning, F. (ed.) Proc. of RTA\u201906. Lecture Notes in Computer Science, vol. 4098, pp. 197\u2013211. Springer, Berlin (2006)"},{"key":"9183_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/3-540-44904-3_20","volume-title":"Proc. of TLCA\u201903","author":"J. Esp\u00edrito Santo","year":"2003","unstructured":"Esp\u00edrito Santo, J., Pinto, L.: Permutative conversions in intuitionistic multiary sequent calculus with cuts. In: Hoffman, M. (ed.) Proc. of TLCA\u201903. Lecture Notes in Computer Science, vol. 2701, pp. 286\u2013300. Springer, Berlin (2003)"},{"key":"9183_CR14","volume-title":"Logic for Computer Science: Foundations of Automated Theorem Proving","author":"J. Gallier","year":"1986","unstructured":"Gallier, J.: Logic for Computer Science: Foundations of Automated Theorem Proving. Wiley, New York (1986)"},{"key":"9183_CR15","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68\u2013131. North-Holland, Amsterdam (1969)"},{"key":"9183_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BFb0022247","volume-title":"Proceedings of CSL\u201994","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.) Proceedings of CSL\u201994. Lecture Notes in Computer Science, vol. 933, pp. 61\u201375. Springer, Berlin (1995)"},{"key":"9183_CR17","first-page":"480","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. 480\u2013490. Academic Press, New York (1980)"},{"key":"9183_CR18","doi-asserted-by":"crossref","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. Arch. Math. Log. 42, 59\u201387 (2003)","journal-title":"Arch. Math. Log."},{"key":"9183_CR19","volume-title":"Introduction to Metamathematics","author":"S. Kleene","year":"1952","unstructured":"Kleene, S.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)"},{"key":"9183_CR20","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Log. 51, 125\u2013157 (1991)","journal-title":"Ann. Pure Appl. Log."},{"key":"9183_CR21","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 (1996)"},{"key":"9183_CR22","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S. Negri","year":"2001","unstructured":"Negri, S., von Plato, J.: Structural Proof Theory. CUP, Cambridge (2001)"},{"key":"9183_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Int. Conf. Logic Prog. Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: \u03bb \u03bc-calculus: an algorithmic interpretation of classic natural deduction. In: Int. Conf. Logic Prog. Automated Reasoning. Lecture Notes in Computer Science, vol. 624, pp. 190\u2013201. Springer, Berlin (1992)"},{"key":"9183_CR24","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0003-4843(77)80004-1","volume":"12","author":"G. Pottinger","year":"1977","unstructured":"Pottinger, G.: Normalization as a homomorphic image of cut-elimination. Ann. Math. Log. 12, 323\u2013357 (1977)","journal-title":"Ann. Math. Log."},{"key":"9183_CR25","volume-title":"Natural Deduction. A Proof-Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction. A Proof-Theoretical Study. Almquist and Wiksell, Stockholm (1965)"},{"key":"9183_CR26","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/S0304-3975(98)00143-1","volume":"212","author":"H. Schwichtenberg","year":"1999","unstructured":"Schwichtenberg, H.: Termination of permutative conversions in intuitionistic Gentzen calculi. Theor. Comput. Sci. 212, 247\u2013260 (1999)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"9183_CR27","first-page":"541","volume":"40","author":"J. Plato von","year":"2001","unstructured":"von Plato, J.: Natural deduction with general elimination rules. Ann. Math. Log. 40(7), 541\u2013567 (2001)","journal-title":"Ann. Math. Log."},{"key":"9183_CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0003-4843(74)90010-2","volume":"7","author":"J. Zucker","year":"1974","unstructured":"Zucker, J.: The correspondence between cut-elimination and normalization. Ann. Math. Log. 7, 1\u2013112 (1974)","journal-title":"Ann. Math. Log."}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-009-9183-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-009-9183-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-009-9183-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T07:51:37Z","timestamp":1558684297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-009-9183-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2,5]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,11]]}},"alternative-id":["9183"],"URL":"https:\/\/doi.org\/10.1007\/s00224-009-9183-9","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2,5]]}}}