{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T12:53:21Z","timestamp":1760014401509,"version":"3.35.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705888"},{"type":"electronic","value":"9783540705901"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70590-1_28","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"409-424","source":"Crossref","is-referenced-by-count":8,"title":["Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof"],"prefix":"10.1007","author":[{"given":"Christian","family":"Urban","sequence":"first","affiliation":[]},{"given":"Bozhi","family":"Zhu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","first-page":"3","volume-title":"Proc.\u00a0of the 35rd Symposium on Principles of Programming Languages (POPL)","author":"B. Aydemir","year":"2008","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering Formal Metatheory. In: Proc.\u00a0of the 35rd Symposium on Principles of Programming Languages (POPL), pp. 3\u201315. ACM, New York (2008)"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-57887-0_112","volume-title":"Theoretical Aspects of Computer Software","author":"F. Barbanera","year":"1994","unstructured":"Barbanera, F., Berardi, S.: A Symmetric Lambda Calculus for \u201cClassical\u201d Program Extraction. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, pp. 495\u2013515. Springer, Heidelberg (1994)"},{"key":"28_CR3","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H. Barendregt","year":"1981","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. North-Holland, Amsterdam (1981)"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Brauner, P., Houtmann, C., Kirchner, C.: Principles of Superdeduction. In: Proc.\u00a0of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 41\u201350 (2007)","DOI":"10.1109\/LICS.2007.37"},{"key":"28_CR5","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen I and II. Mathematische Zeitschrift\u00a039, 176\u2013210, 405\u2013431 (1935)","journal-title":"Mathematische Zeitschrift"},{"issue":"1","key":"28_CR6","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/1042038.1042041","volume":"6","author":"R. Harper","year":"2005","unstructured":"Harper, R., Pfenning, F.: On Equivalence and Canonical Forms in the LF Type Theory. ACM Transactions on Computational Logic\u00a06(1), 61\u2013101 (2005)","journal-title":"ACM Transactions on Computational Logic"},{"key":"28_CR7","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)"},{"issue":"1","key":"28_CR8","doi-asserted-by":"publisher","first-page":"11","DOI":"10.2307\/2963675","volume":"27","author":"S.C. Kleene","year":"1962","unstructured":"Kleene, S.C.: Disjunction and Existence Under Implication in Elementary Intuitionistic Formalisms. Journal of Symbolic Logic\u00a027(1), 11\u201318 (1962)","journal-title":"Journal of Symbolic Logic"},{"issue":"1\u20132","key":"28_CR9","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.1999.2832","volume":"157","author":"F. Pfenning","year":"2000","unstructured":"Pfenning, F.: Structural Cut Elimination. Information and Computation\u00a0157(1\u20132), 84\u2013141 (2000)","journal-title":"Information and Computation"},{"key":"28_CR10","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1145\/1147954.1147961","volume":"53","author":"A. Pitts","year":"2006","unstructured":"Pitts, A.: Alpha-Structural Recursion and Induction. Journal of the ACM\u00a053, 459\u2013506 (2006)","journal-title":"Journal of the ACM"},{"key":"28_CR11","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/S0049-237X(08)70849-8","volume-title":"Proceedings of the 2nd Scandinavian Logic Symposium","author":"D. Prawitz","year":"1971","unstructured":"Prawitz, D.: Ideas and Results of Proof Theory. In: Proceedings of the 2nd Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol.\u00a063, pp. 235\u2013307. North-Holland, Amsterdam (1971)"},{"key":"28_CR12","unstructured":"Sch\u00fcrmann, C., Sarnat, J.: Towards a Judgemental Reconstruction of Logical Relation Proofs. In: Proc.\u00a0of the 23rd IEEE Symposium on Logic in Computer Science (LICS) (to appear, 2008)"},{"key":"28_CR13","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Basic Proof Theory","author":"A.S. Troelstra","year":"1996","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol.\u00a043. Cambridge University Press, Cambridge (1996)"},{"key":"28_CR14","unstructured":"Urban, C.: Classical Logic and Computation. PhD thesis, Cambridge University (October 2000)"},{"key":"28_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/11814771_41","volume-title":"Automated Reasoning","author":"C. Urban","year":"2006","unstructured":"Urban, C., Berghofer, S.: A Recursion Combinator for Nominal Datatypes Implemented in Isabelle\/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 498\u2013512. Springer, Heidelberg (2006)"},{"key":"28_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-73595-3_4","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Urban","year":"2007","unstructured":"Urban, C., Berghofer, S., Norrish, M.: Barendregt\u2019s Variable Convention in Rule Inductions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 35\u201350. Springer, Heidelberg (2007)"},{"issue":"1\u20132","key":"28_CR17","first-page":"123","volume":"45","author":"C. Urban","year":"2001","unstructured":"Urban, C., Bierman, G.: Strong Normalisation of Cut-Elimination in Classical Logic. Fundamenta Informaticae\u00a045(1\u20132), 123\u2013155 (2001)","journal-title":"Fundamenta Informaticae"},{"key":"28_CR18","unstructured":"Urban, C., Cheney, J., Berghofer, S.: Mechanizing the Metatheory of LF. In: Proc.\u00a0of the 23rd IEEE Symposium on Logic in Computer Science (LICS). Technical report (to appear, 2008), http:\/\/isabelle.in.tum.de\/nominal\/LF"},{"key":"28_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/11532231_4","volume-title":"Automated Deduction \u2013 CADE-20","author":"C. Urban","year":"2005","unstructured":"Urban, C., Tasson, C.: Nominal Techniques in Isabelle\/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 38\u201353. Springer, Heidelberg (2005)"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11560586_8","volume-title":"Theoretical Computer Science","author":"S. Bakel van","year":"2005","unstructured":"van Bakel, S., Lengrand, S., Lescanne, P.: The Language X: Circuits, Computations and Classical Logic. In: Coppo, M., Lodi, E., Pinna, G.M. (eds.) ICTCS 2005. LNCS, vol.\u00a03701, pp. 81\u201396. Springer, Heidelberg (2005)"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the \u03c0-Calculus. In: Proc.\u00a0of the 16th IEEE Symposium on Logic in Computer Science (LICS), pp. 311\u2013322 (2001)","DOI":"10.1109\/LICS.2001.932507"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70590-1_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T12:14:37Z","timestamp":1738325677000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70590-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705888","9783540705901"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70590-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}