{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:37:15Z","timestamp":1753889835780,"version":"3.41.2"},"reference-count":38,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2009,5,25]],"date-time":"2009-05-25T00:00:00Z","timestamp":1243209600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The intuitionistic fragment of the call-by-name version of Curien and\nHerbelin's \\lambda\\_mu\\_{\\~mu}-calculus is isolated and proved strongly\nnormalising by means of an embedding into the simply-typed lambda-calculus. Our\nembedding is a continuation-and-garbage-passing style translation, the\ninspiring idea coming from Ikeda and Nakazawa's translation of Parigot's\n\\lambda\\_mu-calculus. The embedding strictly simulates reductions while usual\ncontinuation-passing-style transformations erase permutative reduction steps.\nFor our intuitionistic sequent calculus, we even only need \"units of garbage\"\nto be passed. We apply the same method to other calculi, namely successive\nextensions of the simply-typed &amp;lambda;-calculus leading to our intuitionistic\nsystem, and already for the simplest extension we consider (&amp;lambda;-calculus\nwith generalised application), this yields the first proof of strong\nnormalisation through a reduction-preserving embedding. The results obtained\nextend to second and higher-order calculi.<\/jats:p>","DOI":"10.2168\/lmcs-5(2:11)2009","type":"journal-article","created":{"date-parts":[[2009,9,4]],"date-time":"2009-09-04T06:11:13Z","timestamp":1252044673000},"source":"Crossref","is-referenced-by-count":3,"title":["Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi"],"prefix":"10.46298","volume":"Volume 5, Issue 2","author":[{"given":"Jose Espirito","family":"Santo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7299-2411","authenticated-orcid":false,"given":"Ralph","family":"Matthes","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1338-2688","authenticated-orcid":false,"given":"Luis","family":"Pinto","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2009,5,25]]},"reference":[{"key":"10.2168\/LMCS-5(2:11)2009_BartheHatcliffSoerensen97","doi-asserted-by":"crossref","unstructured":"Gilles Barthe, John Hatcliff, and Morten Heine S\u00f8rensen. A notion of classical pure type system (preliminary version). In Stephen Brookes and Michael Mislove, editors,Proceedings of the Thirteenth Conference on the Mathematical Foundations of Programming Semantics, volume 6 ofElectronic Notes in Theoretical Computer Science. Elsevier, 1997. 56 pp.","DOI":"10.1016\/S1571-0661(05)80170-7"},{"issue":"2","key":"10.2168\/LMCS-5(2:11)2009_BartheHatcliffSoerensen99","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1023\/A:1010000206149","volume":"12","author":"Barthe","year":"1999","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"5","key":"10.2168\/LMCS-5(2:11)2009_BartheSoerensen00","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1017\/S0956796800003750","volume":"10","author":"Barthe","year":"2000","journal-title":"Journal of Functional Programming 2000"},{"issue":"1","key":"10.2168\/LMCS-5(2:11)2009_BlooMSCS2001","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S096012950000325X","volume":"11","author":"Bloo","year":"2001","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.2168\/LMCS-5(2:11)2009_CurienHerbelinFP2000","doi-asserted-by":"crossref","unstructured":"P.-L. Curien and H. Herbelin. The duality of computation. InProceedings of the fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montr\u00e9al, pages 233-243. IEEE, 2000.","DOI":"10.1145\/351240.351262"},{"key":"10.2168\/LMCS-5(2:11)2009_Groote02","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1006\/inco.2002.3147","volume":"178","author":"de Groote","year":"2002","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-5(2:11)2009_Dragalin88","volume-title":"Mathematical Intuitionism., volume 67 of Translations of Mathematical Monographs","author":"Dragalin","year":"1988","edition":"Amer"},{"issue":"5","key":"10.2168\/LMCS-5(2:11)2009_DyckhoffUrbanJLC","doi-asserted-by":"crossref","first-page":"689","DOI":"10.1093\/logcom\/13.5.689","volume":"13","author":"Dyckhoff","year":"2003","journal-title":"Journal of Logic and Computation"},{"key":"10.2168\/LMCS-5(2:11)2009_jesTLCA07","doi-asserted-by":"crossref","unstructured":"J. Esp\u00edrito Santo. Completing Herbelin's programme. In Simona Ronchi della Rocca, editor,Proceedings of TLCA '07, volume 4583 ofLecture Notes in Computer Science, pages 118-132. Springer Verlag, 2007.","DOI":"10.1007\/978-3-540-73228-0_10"},{"key":"10.2168\/LMCS-5(2:11)2009_jesLuisTLCA03","doi-asserted-by":"crossref","unstructured":"J. Esp\u00edrito Santo and Lu\u00eds Pinto. Permutative conversions in intuitionistic multiary sequent calculus with cuts. In M. Hofmann, editor,Proc. of TLCA'03, volume 2701 ofLecture Notes in Computer Science, pages 286-300. Springer-Verlag, 2003.","DOI":"10.1007\/3-540-44904-3_20"},{"key":"10.2168\/LMCS-5(2:11)2009_jesLPintoTYPES03","unstructured":"J. Esp\u00edrito Santo and Lu\u00eds Pinto. Confluence and strong normalisation of the generalised multiary\u03bb-calculus. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors,Revised selected papers from the International Workshop TYPES 2003, volume 3085 ofLecture Notes in Computer Science. Springer-Verlag, 2004."},{"key":"10.2168\/LMCS-5(2:11)2009_ESMP:TLCA07","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Esp\u00edrito Santo, Ralph Matthes, and Lu\u00eds Pinto. Continuation-passing style and strong normalisation for intuitionistic sequent calculi. In Simona Ronchi della Rocca, editor,Proceedings of TLCA '07, volume 4583 ofLecture Notes in Computer Science, pages 133-147. Springer Verlag, 2007.","DOI":"10.1007\/978-3-540-73228-0_11"},{"key":"10.2168\/LMCS-5(2:11)2009_FelleisenFriedmanKohlbeckerDubaLICS1986","unstructured":"M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba. Reasoning with continuations. In1st Symposium on Logic and Computer Science, pages 131-141. IEEE, 1986."},{"key":"10.2168\/LMCS-5(2:11)2009_GeuversCahiers","unstructured":"J. Herman Geuvers. The calculus of constructions and higher order logic. In Ph. de Groote, editor,The Curry-Howard isomorphism, volume 8 ofCahiers du Centre de logique (Universit\u00e9catholique de Louvain), Academia, Louvain-la-Neuve (Belgium), pages 139-191, 1995."},{"key":"10.2168\/LMCS-5(2:11)2009_GirardF","unstructured":"Jean-Yves Girard.Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. Th\u00e8se de Doctorat d'\u00c9tat, Universit\u00e9 de Paris VII, 1972."},{"key":"10.2168\/LMCS-5(2:11)2009_GriffinPOPL1990","doi-asserted-by":"crossref","unstructured":"T. Griffin. A formulae-as-types notion of control. InACM Conf. Principles of Programming Languages, pages 47-58. ACM Press, 1990.","DOI":"10.1145\/96709.96714"},{"issue":"3","key":"10.2168\/LMCS-5(2:11)2009_HarperLillibridgeJFP96","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1017\/S0956796800001775","volume":"6","author":"Harper","year":"1996","journal-title":"J. Funct. Program."},{"key":"10.2168\/LMCS-5(2:11)2009_HerbelinHabilitation","unstructured":"H. Herbelin. C'est maintenant qu'on calcule, 2005. Habilitation Thesis, Paris XI."},{"key":"10.2168\/LMCS-5(2:11)2009_HofmannStreicherJournal","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1006\/inco.2001.2947","volume":"179","author":"Hofmann","year":"2002","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-5(2:11)2009_IkedaNakazawa06","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/j.ipl.2006.03.009","volume":"99","author":"Ikeda","year":"2006","journal-title":"Information Processing Letters"},{"key":"10.2168\/LMCS-5(2:11)2009_JoachimskiMatthesRTA2000","doi-asserted-by":"crossref","unstructured":"F. Joachimski and R. Matthes. Standardization and confluence for a lambda-calculus with generalized applications. In Leo Bachmair, editor,Proc. of Int. Conference on Rewriting Techniques and Applications (RTA 2000), volume 1833 ofLecture Notes in Computer Science, pages 141-155. Springer-Verlag, 2000.","DOI":"10.1007\/10721975_10"},{"issue":"1","key":"10.2168\/LMCS-5(2:11)2009_JoachimskiMatthes03","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/s00153-002-0156-9","volume":"42","author":"Joachimski","year":"2003","journal-title":"Archive for Mathematical Logic"},{"key":"10.2168\/LMCS-5(2:11)2009_LengrandWRS2003","doi-asserted-by":"crossref","unstructured":"S. Lengrand. Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. In B. Gramlich and S. Lucas, editors,Post-proc. of the 3rd Workshop on Reduction Strategies in Rewriting and Programming (WRS'03), volume 86 ofElectronic Notes in Theoretical Computer Science. Elsevier, 2003.","DOI":"10.1016\/S1571-0661(05)82619-2"},{"key":"10.2168\/LMCS-5(2:11)2009_LengrandEtAl06","doi-asserted-by":"crossref","unstructured":"St\u00e9phane Lengrand, Roy Dyckhoff, and James McKinna. A sequent calculus for type theory. In Zolt\u00e1n \u00c9sik, editor,Computer Science Logic, 20th International Workshop, CSL 2006, Proceedings, volume 4207 ofLecture Notes in Computer Science, pages 441-455. Springer Verlag, 2006.","DOI":"10.1007\/11874683_29"},{"key":"10.2168\/LMCS-5(2:11)2009_Likavec:PhD-2005","unstructured":"Silvia Likavec.Types for object-oriented and functional programming languages. PhD thesis, Universit\u00e0 di Torino, Italy, ENS Lyon, France, February 2005."},{"key":"10.2168\/LMCS-5(2:11)2009_Matthes06","doi-asserted-by":"crossref","unstructured":"Ralph Matthes. Stabilization--an alternative to double-negation translation for classical natural deduction. In Viggo Stoltenberg-Hansen and Jouko V\u00e4\u00e4n\u00e4nen, editors,Proceedings of the Logic Colloquium 2003, volume 24 ofLecture Notes in Logic, pages 167-199. A K Peters, 2006.","DOI":"10.1017\/9781316755785.010"},{"key":"10.2168\/LMCS-5(2:11)2009_MayrNipkow98","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"Mayr","year":"1998","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.2168\/LMCS-5(2:11)2009_MunozMSCS2001","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1017\/S0960129500003261","volume":"11","author":"Mu\u00f1oz","year":"2001","journal-title":"Mathematical Structures in Computer Science 2001"},{"issue":"3","key":"10.2168\/LMCS-5(2:11)2009_NakazawaTatsuta03","doi-asserted-by":"crossref","first-page":"851","DOI":"10.2178\/jsl\/1058448444","volume":"68","author":"Nakazawa","year":"2003","journal-title":"Journal of Symbolic Logic \\newblock Corrigendum: vol. 68 (2003), no. 4, pp. 1415-1416"},{"key":"10.2168\/LMCS-5(2:11)2009_NakazawaTatsuta06","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/j.apal.2008.01.003","volume":"153","author":"Nakazawa","year":"2008","journal-title":"Annals of Pure and Applied Logic"},{"issue":"4","key":"10.2168\/LMCS-5(2:11)2009_Parigot97","doi-asserted-by":"crossref","first-page":"1461","DOI":"10.2307\/2275652","volume":"62","author":"Parigot","year":"1997","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-5(2:11)2009_PlotkinTLCA1975","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"Plotkin","year":"1975","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-5(2:11)2009_PolonovskiFOSSACS2004","doi-asserted-by":"crossref","unstructured":"E. Polonovski. Strong normalization of\\bar\u03bb\u03bc\\tilde\u03bc-calculus with explicit substitutions. In Igor Walukiewicz, editor,Proc. of 7th Int. Conference on Foundations of Software Sciences and Computation Structures (FoSSaCS 2004), volume 2987 ofLecture Notes in Computer Science, pages 423-437. Springer-Verlag, 2004.","DOI":"10.1007\/978-3-540-24727-2_30"},{"key":"10.2168\/LMCS-5(2:11)2009_SabryWadlerFP1996","doi-asserted-by":"crossref","unstructured":"A. Sabry and P. Wadler. A reflection on call-by-value. InProc. of ACM SIGPLAN Int. Conference on Functional Programming ICFP 1996, pages 13-24. ACM Press, 1996.","DOI":"10.1145\/232629.232631"},{"issue":"1-2","key":"10.2168\/LMCS-5(2:11)2009_SchwichtenbergTCS1999","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/S0304-3975(98)00143-1","volume":"212","author":"Schwichtenberg","year":"1999","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"10.2168\/LMCS-5(2:11)2009_SeldinTCS2000","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/S0304-3975(98)00195-9","volume":"243","author":"Seldin","year":"2000","journal-title":"Theor. Comput. Sci."},{"key":"10.2168\/LMCS-5(2:11)2009_Tait75","doi-asserted-by":"crossref","unstructured":"William W. Tait. A realizability interpretation of the theory of species. In Rohit Parikh, editor,Logic Colloquium Boston 1971\/72, volume 453 ofLecture Notes in Mathematics, pages 240-251. Springer Verlag, 1975.","DOI":"10.1007\/BFb0064875"},{"key":"10.2168\/LMCS-5(2:11)2009_UrbanBiermanTLCA1999","doi-asserted-by":"crossref","unstructured":"C. Urban and G. Bierman. Strong normalisation of cut-elimination in classical logic. In Jean-Yves Girard, editor,Proceedings of TLCA'99, volume 1581 ofLecture Notes in Computer Science, pages 365-380. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48959-2_26"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1149\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1149\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:04:38Z","timestamp":1681243478000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1149"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,5,25]]},"references-count":38,"URL":"https:\/\/doi.org\/10.2168\/lmcs-5(2:11)2009","relation":{"is-same-as":[{"id-type":"arxiv","id":"0903.1822","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0903.1822","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2009,5,25]]},"article-number":"1149"}}