{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:58:54Z","timestamp":1725562734676},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642152047"},{"type":"electronic","value":"9783642152054"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15205-4_24","type":"book-chapter","created":{"date-parts":[[2010,8,13]],"date-time":"2010-08-13T14:48:24Z","timestamp":1281710904000},"page":"290-304","source":"Crossref","is-referenced-by-count":1,"title":["Towards a Canonical Classical Natural Deduction System"],"prefix":"10.1007","author":[{"given":"Jos\u00e9 Esp\u00edrito","family":"Santo","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"24_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. Journal of Functional Programming\u00a01(4), 375\u2013416 (1991)","journal-title":"Journal of Functional Programming"},{"issue":"5","key":"24_CR2","doi-asserted-by":"publisher","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. Journal of Logic and Computation\u00a013(5), 639\u2013688 (2003)","journal-title":"Journal of Logic and Computation"},{"key":"24_CR3","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/351240.351262","volume-title":"Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000)","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), Montreal, Canada, September 18-21. SIGPLAN Notices, vol.\u00a035(9), pp. 233\u2013243. ACM, New York (2000)"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"1109","DOI":"10.1093\/logcom\/exm037","volume":"17","author":"R. Dyckhoff","year":"2007","unstructured":"Dyckhoff, R., Lengrand, S.: Call-by-value lambda calculus and LJQ. Journal of Logic and Computation\u00a017, 1109\u20131134 (2007)","journal-title":"Journal of Logic and Computation"},{"key":"24_CR5","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":"24_CR6","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":"24_CR7","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/s00224-009-9183-9","volume":"45","author":"J. Esp\u00edrito Santo","year":"2009","unstructured":"Esp\u00edrito Santo, J.: The \u03bb-calculus and the unity of structural proof theory. Theory of Computing Systems\u00a045, 963\u2013994 (2009)","journal-title":"Theory of Computing Systems"},{"key":"24_CR8","volume-title":"1st Symposium on Logic and Computer Science","author":"M. Felleisen","year":"1986","unstructured":"Felleisen, M., Friedman, D., Kohlbecker, E., Duba, B.: Reasoning with continuations. In: 1st Symposium on Logic and Computer Science. IEEE, Los Alamitos (1986)"},{"key":"24_CR9","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":"24_CR10","volume-title":"ACM Conf. Principles of Programming Languages","author":"T. Griffin","year":"1990","unstructured":"Griffin, T.: A formulae-as-types notion of control. In: ACM Conf. Principles of Programming Languages. ACM Press, New York (1990)"},{"key":"24_CR11","unstructured":"Herbelin, H.: C\u2019est maintenant qu\u2019on calcule, Habilitation Thesis (2005)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-02273-9_12","volume-title":"Typed Lambda Calculi and Applications","author":"H. Herbelin","year":"2009","unstructured":"Herbelin, H., Zimmermann, S.: An operational account of call-by-value minimal and classical lambda-calculus in \u201cnatural deduction\u201d form. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 142\u2013156. Springer, Heidelberg (2009)"},{"key":"24_CR13","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.apal.2008.01.002","volume":"153","author":"K. Kikuchi","year":"2008","unstructured":"Kikuchi, K.: Call-by-name reduction and cut-elimination in classical logic. Annals of Pure and Applied Logic\u00a0153, 38\u201365 (2008)","journal-title":"Annals of Pure and Applied Logic"},{"key":"24_CR14","unstructured":"Moggi, E.: Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-86, University of Edinburgh (1988)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Negri, S., von Plato, J.: Structural Proof Theory, Cambridge (2001)","DOI":"10.1017\/CBO9780511527340"},{"key":"24_CR16","first-page":"215","volume-title":"Proc. of Symposium on Principles of Programming Languages (POPL 1997)","author":"C.-H.L. Ong","year":"1997","unstructured":"Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: Proc. of Symposium on Principles of Programming Languages (POPL 1997), pp. 215\u2013217. ACM Press, New York (1997)"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: \u03bb\u03bc-calculus: an algorithmic interpretation of classic natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"24_CR18","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. Plotkin","year":"1975","unstructured":"Plotkin, G.: Call-by-name, call-by-value and the \u03bb-calculus. Theoretical Computer Science\u00a01, 125\u2013159 (1975)","journal-title":"Theoretical Computer Science"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-540-24727-2_30","volume-title":"Foundations of Software Science and Computation Structures","author":"E. Polonovski","year":"2004","unstructured":"Polonovski, E.: Strong normalization of lambda-mu-mu-tilde with explicit substitutions. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 423\u2013437. Springer, Heidelberg (2004)"},{"key":"24_CR20","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":"24_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Theoretical Aspects of Computer Software","author":"N. Rehof","year":"1994","unstructured":"Rehof, N., Sorensen, M.: The \u03bb\n                  \u0394-calculus. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789. Springer, Heidelberg (1994)"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/978-3-540-32033-3_16","volume-title":"Term Rewriting and Applications","author":"J. Rocheteau","year":"2005","unstructured":"Rocheteau, J.: \u03bb\u03bc-calculus and duality: call-by-name and call-by-value. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 204\u2013218. Springer, Heidelberg (2005)"},{"issue":"3\/4","key":"24_CR23","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01019462","volume":"6","author":"A. Sabry","year":"1993","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programms in continuation-passing-style. LISP and Symbolic Computation\u00a06(3\/4), 289\u2013360 (1993)","journal-title":"LISP and Symbolic Computation"},{"issue":"6","key":"24_CR24","doi-asserted-by":"publisher","first-page":"916","DOI":"10.1145\/267959.269968","volume":"19","author":"A. Sabry","year":"1997","unstructured":"Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Transactions on Programming Languages and Systems\u00a019(6), 916\u2013941 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR25","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"A. Troelstra","year":"2000","unstructured":"Troelstra, A., Schwitchtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)","edition":"2"},{"issue":"7","key":"24_CR26","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001530100091","volume":"40","author":"J. von Plato","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","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15205-4_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:02:28Z","timestamp":1606186948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15205-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642152047","9783642152054"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15205-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}