{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T16:25:21Z","timestamp":1648657521442},"reference-count":31,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2013,1,18]],"date-time":"2013-01-18T00:00:00Z","timestamp":1358467200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2013,12]]},"abstract":"<jats:p>We study monadic translations of the call-by-name (cbn) and call-by-value (cbv) fragments of the classical sequent calculus <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129512000436_inline1\" \/><jats:tex-math>${\\overline{\\lambda}\\mu\\tilde{\\mu}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> due to Curien and Herbelin, and give modular and syntactic proofs of strong normalisation. The target of the translations is a new meta-language for classical logic, named monadic \u03bb\u03bc. This language is a monadic reworking of Parigot's \u03bb\u03bc-calculus, where the monadic binding is confined to commands, thus integrating the monad with the classical features. Also, its \u03bc-reduction rule is replaced by a rule expressing the interaction between monadic binding and \u03bc-abstraction.<\/jats:p><jats:p>Our monadic translations produce very tight simulations of the respective fragments of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129512000436_inline1\" \/><jats:tex-math>${\\overline{\\lambda}\\mu\\tilde{\\mu}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> within monadic \u03bb\u03bc, with reduction steps of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129512000436_inline1\" \/><jats:tex-math>${\\overline{\\lambda}\\mu\\tilde{\\mu}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> being translated in a 1\u20131 fashion, except for \u03b2 steps, which require two steps. The monad of monadic \u03bb\u03bc can be instantiated to the continuations monad so as to ensure strict simulation of monadic \u03bb\u03bc within simply typed \u03bb-calculus with \u03b2- and \u03b7-reduction. Through strict simulation, the strong normalisation of simply typed \u03bb-calculus is inherited by monadic \u03bb\u03bc, and then by cbn and cbv <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129512000436_inline1\" \/><jats:tex-math>${\\overline{\\lambda}\\mu\\tilde{\\mu}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, thus reproving strong normalisation in an elementary syntactical way for these fragments of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129512000436_inline1\" \/><jats:tex-math>${\\overline{\\lambda}\\mu\\tilde{\\mu}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, and establishing it for our new calculus. These results extend to second-order logic, with polymorphic \u03bb-calculus as the target, giving new strong normalisation results for classical second-order logic in sequent calculus style.<\/jats:p><jats:p>CPS translations of cbn and cbv <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129512000436_inline1\" \/><jats:tex-math>${\\overline{\\lambda}\\mu\\tilde{\\mu}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> with the strict simulation property are obtained by composing our monadic translations with the continuations-monad instantiation. In an appendix to the paper, we investigate several refinements of the continuations-monad instantiation in order to obtain in a modular way improvements of the CPS translations enjoying extra properties like simulation by cbv \u03b2-reduction or reduction of administrative redexes at compile time.<\/jats:p>","DOI":"10.1017\/s0960129512000436","type":"journal-article","created":{"date-parts":[[2013,1,18]],"date-time":"2013-01-18T14:43:02Z","timestamp":1358520182000},"page":"1111-1162","source":"Crossref","is-referenced-by-count":1,"title":["Monadic translation of classical sequent calculus"],"prefix":"10.1017","volume":"23","author":[{"given":"JOS\u00c9","family":"ESP\u00cdRITO SANTO","sequence":"first","affiliation":[]},{"given":"RALPH","family":"MATTHES","sequence":"additional","affiliation":[]},{"given":"KOJI","family":"NAKAZAWA","sequence":"additional","affiliation":[]},{"given":"LU\u00cdS","family":"PINTO","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2013,1,18]]},"reference":[{"key":"S0960129512000436_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_16"},{"key":"S0960129512000436_ref10","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(2:11)2009"},{"key":"S0960129512000436_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019463"},{"key":"S0960129512000436_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"S0960129512000436_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02444-3_7"},{"key":"S0960129512000436_ref23","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1058448444"},{"key":"S0960129512000436_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_13"},{"key":"S0960129512000436_ref8","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm037"},{"key":"S0960129512000436_ref30","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzq013"},{"key":"S0960129512000436_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003750"},{"key":"S0960129512000436_ref13","unstructured":"Geuvers H. (1993) Logics and Type Systems, Proefschrift (Ph.D. thesis), University of Nijmegen."},{"key":"S0960129512000436_ref25","doi-asserted-by":"publisher","DOI":"10.2307\/2275652"},{"key":"S0960129512000436_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15240-5_13"},{"key":"S0960129512000436_ref4","doi-asserted-by":"crossref","unstructured":"Curien P.-L. and Herbelin H. (2000) The duality of computation. In: Proceedings of ICFP 2000, IEEE 233\u2013243. (Errata available from the second author's homepage.)","DOI":"10.1145\/351240.351262"},{"key":"S0960129512000436_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001535"},{"key":"S0960129512000436_ref18","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2947"},{"key":"S0960129512000436_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"S0960129512000436_ref17","unstructured":"Herbelin H. (2005) C'est maintenant qu'on calcule \u2013 au c\u0153ur de la dualit\u00e9, Habilitation thesis, University Paris 11."},{"key":"S0960129512000436_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/10703163_20"},{"key":"S0960129512000436_ref31","unstructured":"Urban C. (2000) Classical Logic and Computation, Ph.D. thesis, University of Cambridge."},{"key":"S0960129512000436_ref16","first-page":"458","volume-title":"Proceedings of POPL 1994","author":"Hatcliff","year":"1994"},{"key":"S0960129512000436_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129512000436_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82619-2"},{"key":"S0960129512000436_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_30"},{"key":"S0960129512000436_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00012-3"},{"key":"S0960129512000436_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_9"},{"key":"S0960129512000436_ref7","first-page":"489","article-title":"Arithmetical proofs of strong normalization results for symmetric \u03bb-calculi.","volume":"77","author":"David","year":"2007","journal-title":"Fundamenta Informaticae"},{"key":"S0960129512000436_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2006.03.009"},{"key":"S0960129512000436_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0960129512000436_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_11"},{"key":"S0960129512000436_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269968"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129512000436","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T02:27:35Z","timestamp":1555986455000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129512000436\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,18]]},"references-count":31,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["S0960129512000436"],"URL":"https:\/\/doi.org\/10.1017\/s0960129512000436","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,1,18]]}}}