{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:53:35Z","timestamp":1725551615064},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540305538"},{"type":"electronic","value":"9783540316503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11591191_13","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T09:44:25Z","timestamp":1132652665000},"page":"169-183","source":"Crossref","is-referenced-by-count":2,"title":["Strong Normalization of the Dual Classical Sequent Calculus"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Dougherty","sequence":"first","affiliation":[]},{"given":"Silvia","family":"Ghilezan","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Lescanne","sequence":"additional","affiliation":[]},{"given":"Silvia","family":"Likavec","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"871","DOI":"10.1007\/3-540-45061-0_68","volume-title":"Automata, Languages and Programming","author":"Z.M. Ariola","year":"2003","unstructured":"Ariola, Z.M., Herbelin, H.: Minimal classical logic and control operators. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 871\u2013885. Springer, Heidelberg (2003)"},{"key":"13_CR2","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","year":"2005","unstructured":"Bakel, S.: The language \n \n \n \n $\\mathcal{X}$\n : 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)"},{"issue":"2","key":"13_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0025","volume":"125","author":"F. Barbanera","year":"1996","unstructured":"Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Information and Computation\u00a0125(2), 103\u2013117 (1996)","journal-title":"Information and Computation"},{"volume-title":"The Lambda Calculus: its Syntax and Semantics","year":"1984","author":"H.P. Barendregt","key":"13_CR4","unstructured":"Barendregt, H.P.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984) (revised edition)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/BFb0055783","volume-title":"Mathematical Foundations of Computer Science 1998","author":"G.M. Bierman","year":"1998","unstructured":"Bierman, G.M.: A computational interpretation of the \u03bb\u03bc-calculus. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol.\u00a01450, pp. 336\u2013345. Springer, Heidelberg (1998)"},{"issue":"3","key":"13_CR6","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1017\/S0960129500000505","volume":"4","author":"R.D. Cosmo","year":"1994","unstructured":"Cosmo, R.D., Kesner, D.: Simulating expansions without expansions. Mathematical Structures in Computer Science\u00a04(3), 315\u2013362 (1994)","journal-title":"Mathematical Structures in Computer Science"},{"key":"13_CR7","unstructured":"Curien, P.-L.: Symmetry and interactivity in programming. Archive for Mathematical Logic (2001) (to appear)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/3-540-45699-6_3","volume-title":"Applied Semantics","author":"P.-L. Curien","year":"2002","unstructured":"Curien, P.-L.: Abstract machines, control, and sequents. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol.\u00a02395, pp. 123\u2013136. Springer, Heidelberg (2002)"},{"volume-title":"Proc. of the 5th ACM SIGPLAN Int. Conference on Functional Programming (ICFP 2000)","year":"2000","author":"P.-L. Curien","key":"13_CR9","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Proc. of the 5th ACM SIGPLAN Int. Conference on Functional Programming (ICFP 2000), Montreal, Canada. ACM Press, New York (2000)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11417170_13","volume-title":"Typed Lambda Calculi and Applications","author":"R. David","year":"2005","unstructured":"David, R., Nour, K.: Arithmetical proofs of strong normalization results for the symmetric \u03bb\u03bc-calculus. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 162\u2013178. Springer, Heidelberg (2005)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-58216-9_27","volume-title":"Logic Programming and Automated Reasoning","author":"P. Groote de","year":"1994","unstructured":"de Groote, P.: On the relation between the \u03bb\u03bc-calculus and the syntactic theory of sequential control. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol.\u00a0822, pp. 31\u201343. Springer, Heidelberg (1994)"},{"key":"13_CR12","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1145\/1013963.1013982","volume-title":"Sixth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming PPDP 2004","author":"D. Dougherty","year":"2004","unstructured":"Dougherty, D., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in a language with control operators. In: Sixth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming PPDP 2004, pp. 155\u2013166. ACM Press, New York (2004)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-56868-9_12","volume-title":"Rewriting Techniques and Applications","author":"D.J. Dougherty","year":"1993","unstructured":"Dougherty, D.J.: Some lambda calculi with categorical sums and products. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 137\u2013151. Springer, Heidelberg (1993)"},{"key":"13_CR14","unstructured":"Filinski, A.: Declarative continuations and categorical duality. Master\u2019s thesis, DIKU, Computer Science Department, University of Copenhagen, DIKU Rapport 89\/11 (August 1989)"},{"first-page":"68","volume-title":"Collected papers of Gerhard Gentzen","year":"1969","key":"13_CR15","unstructured":"Gentzen, G.: Unterschungen \u00fcber das logische Schliessen, Math Z., vol.\u00a039, pp. 176\u2013210 (1935); Szabo, M. (ed.): Collected papers of Gerhard Gentzen, pp. 68\u2013131. North-Holland, Amsterdam (1969)"},{"key":"13_CR16","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1145\/96709.96714","volume":"17","author":"T. Griffin","year":"1990","unstructured":"Griffin, T.: A formulae-as-types notion of control. POPL\u00a017, 47\u201358 (1990)","journal-title":"POPL"},{"key":"13_CR17","unstructured":"Herbelin, H.: S\u00e9quents qu\u2019on calcule\u00a0: de l\u2019interpr\u00e9tation du calcul des s\u00e9quents comme calcul de \u03bb-termes et comme calcul de strat\u00e9gies gagnantes. Th\u00e8se, U. Paris 7, Janvier (1995)"},{"key":"13_CR18","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 formulas-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, New York, pp. 479\u2013490. Academic Press, London (1980)"},{"volume-title":"ENTCS","year":"2003","author":"S. Lengrand","key":"13_CR19","unstructured":"Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. In: Gramlich, B., Lucas, S. (eds.) ENTCS, vol.\u00a086. Elsevier, Amsterdam (2003)"},{"key":"13_CR20","unstructured":"Likavec, S.: Types for object oriented and functional programming languages. PhD thesis, Universit\u00e0 di Torino, Italy, ENS Lyon, France (2005)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/BFb0021084","volume-title":"Constructivity in Computer Science","author":"C.R. Murthy","year":"1992","unstructured":"Murthy, C.R.: Classical proofs as programs: How, what, and why. In: Myers Jr., J.P., O\u2019Donnell, M.J. (eds.) Constructivity in CS 1991. LNCS, vol.\u00a0613, pp. 71\u201388. Springer, Heidelberg (1992)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: POPL, vol.\u00a024, pp. 215\u2013227 (1997)","DOI":"10.1145\/263699.263722"},{"key":"13_CR23","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.: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"issue":"4","key":"13_CR24","doi-asserted-by":"publisher","first-page":"1461","DOI":"10.2307\/2275652","volume":"62","author":"M. Parigot","year":"1997","unstructured":"Parigot, M.: Proofs of strong normalisation for second order classical natural deduction. The J. of Symbolic Logic\u00a062(4), 1461\u20131479 (1997)","journal-title":"The J. of Symbolic Logic"},{"key":"13_CR25","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 \n \n \n \n $\\lambda\\mu\\tilde{\\mu}$\n -calculus with explicit substitutions. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 423\u2013437. Springer, Heidelberg (2004)"},{"key":"13_CR26","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/S0022-4049(00)00161-4","volume":"159","author":"D. Pym","year":"2001","unstructured":"Pym, D., Ritter, E.: On the semantics of classical disjunction. J. of Pure and Applied Algebra\u00a0159, 315\u2013338 (2001)","journal-title":"J. of Pure and Applied Algebra"},{"issue":"2","key":"13_CR27","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1017\/S096012950000311X","volume":"11","author":"P. Selinger","year":"2001","unstructured":"Selinger, P.: Control categories and duality: On the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science\u00a011(2), 207\u2013260 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"key":"13_CR28","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M. Takahashi","year":"1995","unstructured":"Takahashi, M.: Parallel reduction in \u03bb-calculus. Information and Computation\u00a0118, 120\u2013127 (1995)","journal-title":"Information and Computation"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-48959-2_26","volume-title":"Typed Lambda Calculi and Applications","author":"C. Urban","year":"1999","unstructured":"Urban, C., Bierman, G.M.: Strong normalisation of cut-elimination in classical logic. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 365\u2013380. Springer, Heidelberg (1999)"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Call-by-value is dual to call-by-name. In: Proc. of the 8th Int. Conference on Functional Programming, pp. 189\u2013201 (2003)","DOI":"10.1145\/944705.944723"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-540-32033-3_15","volume-title":"Term Rewriting and Applications","author":"P. Wadler","year":"2005","unstructured":"Wadler, P.: Call-by-value is dual to call-by-name, reloaded. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 185\u2013203. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11591191_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:51:27Z","timestamp":1619506287000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11591191_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540305538","9783540316503"],"references-count":31,"URL":"http:\/\/dx.doi.org\/10.1007\/11591191_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}
