{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:58:28Z","timestamp":1725487108602},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540732273"},{"type":"electronic","value":"9783540732280"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73228-0_11","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:57:11Z","timestamp":1184601431000},"page":"133-147","source":"Crossref","is-referenced-by-count":3,"title":["Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Esp\u00edrito Santo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralph","family":"Matthes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lu\u00eds","family":"Pinto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"56","volume-title":"Proc. of the 30th Conf. on the Mathematical Foundations of Programming Semantics","author":"G. Barthe","year":"1997","unstructured":"Barthe, G., Hatcliff, J., S\u00f8rensen, M.: A notion of classical pure type system (preliminary version). In: Brookes, S., Mislove, M. (eds.) Proc. of the 30th Conf. on the Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol.\u00a06, p. 56. Elsevier, Amsterdam (1997)"},{"issue":"2","key":"11_CR2","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1023\/A:1010000206149","volume":"12","author":"G. Barthe","year":"1999","unstructured":"Barthe, G., Hatcliff, J., S\u00f8rensen, M.: Cps translations and applications: The cube and beyond. Higher-Order and Symbolic Computation\u00a012(2), 125\u2013170 (1999)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/351240.351262","volume-title":"ICFP \u201900","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP \u201900. Proc. of 5th ACM SIGPLAN Int. Conf. on Functional Programming, Montr\u00e9al, pp. 233\u2013243. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1006\/inco.2002.3147","volume":"178","author":"P. Groote de","year":"2002","unstructured":"de Groote, P.: On the strong normalisation of intuitionistic natural deduction with permutation-conversions. Information and Computation\u00a0178, 441\u2013464 (2002)","journal-title":"Information and Computation"},{"key":"11_CR5","unstructured":"Dragalin, A.: Mathematical Intuitionism. Translations of Mathematical Monographs, vol.\u00a067. AMS (1988)"},{"issue":"5","key":"11_CR6","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1093\/logcom\/13.5.689","volume":"13","author":"R. Dyckhoff","year":"2003","unstructured":"Dyckhoff, R., Urban, C.: Strong normalisation of Herbelin\u2019s explicit substitution calculus with substitution propagation. Journal of Logic and Computation\u00a013(5), 689\u2013706 (2003)","journal-title":"Journal of Logic and Computation"},{"key":"11_CR7","unstructured":"Esp\u00edrito Santo, J.: Completing Herbelin\u2019s programme (in this volume)."},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/3-540-44904-3_20","volume-title":"Typed Lambda Calculi and Applications","author":"J. Esp\u00edrito Santo","year":"2003","unstructured":"Esp\u00edrito Santo, J., 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":"11_CR9","first-page":"131","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, pp. 131\u2013141. IEEE Computer Society Press, Los Alamitos (1986)"},{"key":"11_CR10","first-page":"47","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, pp. 47\u201358. ACM Press, New York (1990)"},{"key":"11_CR11","unstructured":"Herbelin, H.: C\u2019est maintenant qu\u2019on calcule, Habilitation Thesis, Paris XI (2005)"},{"key":"11_CR12","first-page":"387","volume-title":"Proc. of LICS 1997","author":"M. Hofmann","year":"1997","unstructured":"Hofmann, M., Streicher, T.: Continuation models are universal for lambda-mu-calculus. In: Proc. of LICS 1997, pp. 387\u2013395. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.ipl.2006.03.009","volume":"99","author":"S. Ikeda","year":"2006","unstructured":"Ikeda, S., Nakazawa, K.: Strong normalization proofs by CPS-translations. Information Processing Letters\u00a099, 163\u2013170 (2006)","journal-title":"Information Processing Letters"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/10721975_10","volume-title":"Rewriting Techniques and Applications","author":"F. Joachimski","year":"2000","unstructured":"Joachimski, F., Matthes, R.: Standardization and confluence for a lambda-calculus with generalized applications. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 141\u2013155. Springer, Heidelberg (2000)"},{"issue":"1","key":"11_CR15","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(1), 59\u201387 (2003)","journal-title":"Archive for Mathematical Logic"},{"key":"11_CR16","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"WRS\u201903","author":"S. Lengrand","year":"2003","unstructured":"Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. In: Gramlich, B., Lucas, S. (eds.) WRS\u201903. Post-proc. of the 3rd Workshop on Reduction Strategies in Rewriting and Programming. Electronic Notes in Theoretical Computer Science, vol.\u00a086, Elsevier, Amsterdam (2003)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11874683_29","volume-title":"Computer Science Logic","author":"S. Lengrand","year":"2006","unstructured":"Lengrand, S., Dyckhoff, R., McKinna, J.: A sequent calculus for type theory. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, pp. 441\u2013455. Springer, Heidelberg (2006)"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R. Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science\u00a0192, 3\u201329 (1998)","journal-title":"Theoretical Computer Science"},{"key":"11_CR19","unstructured":"Nakazawa, K., Tatsuta, M.: Strong normalization of classical natural deduction with disjunctions (Submitted)"},{"issue":"3","key":"11_CR20","doi-asserted-by":"crossref","first-page":"851","DOI":"10.2178\/jsl\/1058448444","volume":"68","author":"K. Nakazawa","year":"2003","unstructured":"Nakazawa, K., Tatsuta, M.: Strong normalization proof with CPS-translation for second order classical natural deduction. Journal of Symbolic Logic\u00a068(3), 851\u2013859 (2003), Corrigendum: 68(4), 1415\u20131416 (2003)","journal-title":"Journal of Symbolic Logic"},{"key":"11_CR21","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":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"11_CR23","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/232627.232631","volume-title":"Proc. of ACM SIGPLAN Int. Conf. on Functional Programming ICFP 1996","author":"A. Sabry","year":"1996","unstructured":"Sabry, A., Wadler, P.: A reflection on call-by-value. In: Proc. of ACM SIGPLAN Int. Conf. on Functional Programming ICFP 1996, pp. 13\u201324. ACM Press, New York (1996)"},{"issue":"1-2","key":"11_CR24","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a0212(1-2), 247\u2013260 (1999)","journal-title":"Theoretical Computer Science"},{"key":"11_CR25","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.: Strong normalisation of cut-elimination in classical logic. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 365\u2013380. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73228-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T00:41:47Z","timestamp":1550450507000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73228-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540732273","9783540732280"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73228-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}