{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T00:40:13Z","timestamp":1739148013823,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642024436"},{"type":"electronic","value":"9783642024443"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02444-3_7","type":"book-chapter","created":{"date-parts":[[2009,6,6]],"date-time":"2009-06-06T09:15:35Z","timestamp":1244279735000},"page":"100-116","source":"Crossref","is-referenced-by-count":2,"title":["Monadic Translation of Intuitionistic Sequent Calculus"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Esp\u00edrito Santo","sequence":"first","affiliation":[]},{"given":"Ralph","family":"Matthes","sequence":"additional","affiliation":[]},{"given":"Lu\u00eds","family":"Pinto","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","first-page":"233","volume-title":"Proc. of 5th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2000)","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Proc. of 5th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2000), Montr\u00e9al, pp. 233\u2013243. IEEE, Los Alamitos (2000)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-73228-0_10","volume-title":"Typed Lambda Calculi and Applications","author":"J. Esp\u00edrito Santo","year":"2007","unstructured":"Esp\u00edrito Santo, J.: Completing Herbelin\u2019s programme. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 118\u2013132. Springer, Heidelberg (2007)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-73449-9_14","volume-title":"Term Rewriting and Applications","author":"J. Esp\u00edrito Santo","year":"2007","unstructured":"Esp\u00edrito Santo, J.: Delayed substitutions. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 169\u2013183. Springer, Heidelberg (2007)"},{"key":"7_CR4","unstructured":"Esp\u00edrito Santo, J.: Addenda to Delayed Substitutions (2008) (manuscript available from the author\u2019s web page)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-540-73228-0_11","volume-title":"Typed Lambda Calculi and Applications","author":"J. Esp\u00edrito Santo","year":"2007","unstructured":"Esp\u00edrito Santo, J., Matthes, R., Pinto, L.: Continuation-passing style and strong normalisation for intuitionistic sequent calculi. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 133\u2013147. Springer, Heidelberg (2007)"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito Santo, J., Matthes, R., Pinto, L.: Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Logical Methods in Computer Science (to appear, 2009)","DOI":"10.2168\/LMCS-5(2:11)2009"},{"key":"7_CR7","first-page":"458","volume-title":"POPL 1994: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"J. Hatcliff","year":"1994","unstructured":"Hatcliff, J., Danvy, O.: A generic account of continuation-passing styles. In: POPL 1994: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 458\u2013471. ACM, New York (1994)"},{"key":"7_CR8","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":"7_CR9","doi-asserted-by":"crossref","unstructured":"Kfoury, A.J., Wells, J.B.: New notions of reduction and non-semantic proofs of beta-strong normalisation in typed lambda-calculi. In: Proceedings of LICS 1995, pp. 311\u2013321 (1995)","DOI":"10.1109\/LICS.1995.523266"},{"key":"7_CR10","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Post-proc. of the 3rd Workshop on Reduction Strategies in Rewriting and Programming (WRS 2003)","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.) Post-proc. of the 3rd Workshop on Reduction Strategies in Rewriting and Programming (WRS 2003). Electronic Notes in Theoretical Computer Science, vol.\u00a086, Elsevier, Amsterdam (2003)"},{"key":"7_CR11","unstructured":"Lengrand, S.: Temination of lambda-calculus with the extra call-by-value rule known as assoc. arXiv:0806.4859v2 (2007)"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput.\u00a093(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"7_CR13","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 $\\overline{\\lambda}\\mu\\tilde{\\mu}$ with explicit substitutions. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 423\u2013437. Springer, Heidelberg (2004)"},{"issue":"3","key":"7_CR14","doi-asserted-by":"publisher","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. Annals of Mathematical Logic\u00a012(3), 323\u2013357 (1977)","journal-title":"Annals of Mathematical Logic"},{"issue":"2","key":"7_CR15","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0304-3975(94)90012-4","volume":"126","author":"L. Regnier","year":"1994","unstructured":"Regnier, L.: Une \u00e9quivalence sur les lambda-termes. Theoretical Computer Science\u00a0126(2), 281\u2013292 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"7_CR16","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 Trans. Program. Lang. Syst.\u00a019(6), 916\u2013941 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"7_CR17","doi-asserted-by":"publisher","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. Annals of Mathematical Logic\u00a07(1), 1\u2013112 (1974)","journal-title":"Annals of Mathematical Logic"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02444-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T00:05:14Z","timestamp":1739145914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02444-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642024436","9783642024443"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02444-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}