{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,22]],"date-time":"2023-08-22T11:40:26Z","timestamp":1692704426424},"reference-count":25,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2017,2,27]],"date-time":"2017-02-27T00:00:00Z","timestamp":1488153600000},"content-version":"unspecified","delay-in-days":57,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Designing rewriting systems that respect functional extensionality for call-by-name languages with effects turns out to be surprisingly challenging. Simply interpreting extensional laws like \u03b7 as reduction rules easily breaks confluence. We explore these issues in the setting of a sequent calculus. Building on an insight that appears in different aspects of the theory of call-by-name functional languages\u2014confluent rewriting for two independent control calculi and sound continuation-passing style transformations\u2014we give a confluent reduction system for lazy extensional functions. Finally, we consider limitations to this approach when used for strict evaluation and types beyond functions.<\/jats:p>","DOI":"10.1017\/s095679681700003x","type":"journal-article","created":{"date-parts":[[2017,2,27]],"date-time":"2017-02-27T01:36:36Z","timestamp":1488159396000},"source":"Crossref","is-referenced-by-count":1,"title":["Call-by-name extensionality and confluence"],"prefix":"10.1017","volume":"27","author":[{"given":"PHILIP","family":"JOHNSON-FREYD","sequence":"first","affiliation":[]},{"given":"PAUL","family":"DOWNEN","sequence":"additional","affiliation":[]},{"given":"ZENA M.","family":"ARIOLA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,2,27]]},"reference":[{"key":"S095679681700003X_ref3","unstructured":"Carraro A. , Ehrhard T. & Salibra A. (2012) The stack calculus. In Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2012, Rio de Janeiro, Brazil, September 29\u201330, 2012, pp. 93\u2013108."},{"key":"S095679681700003X_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90014-X"},{"key":"S095679681700003X_ref15","doi-asserted-by":"crossref","unstructured":"Munch-Maccagnoni G. (2013) Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD Thesis, Universit\u00e9 Paris Diderot.","DOI":"10.1007\/978-3-642-54830-7_26"},{"key":"S095679681700003X_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00104-X"},{"key":"S095679681700003X_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"S095679681700003X_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"key":"S095679681700003X_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269968"},{"key":"S095679681700003X_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S095679681700003X_ref17","unstructured":"Nakazawa K. & Nagai T. (2014) Reduction system for extensional lambda-mu calculus. In Rewriting and Typed Lambda Calculi: Joint International Conference, Rta-Tlca 2014, held as part of the Vienna Summer of Logic, vsl 2014, Dowek G. (ed), Vienna, Austria, July 14\u201317, 2014. Proceedings. LNCS. Cham: Springer International Publishing, pp. 349\u2013363."},{"key":"S095679681700003X_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"S095679681700003X_ref6","doi-asserted-by":"crossref","unstructured":"Danvy O. & Nielsen L. R. (2004) Refocusing in Reduction Semantics. Technical Report BRICS. Danish National Research Foundation.","DOI":"10.7146\/brics.v11i26.21851"},{"key":"S095679681700003X_ref5","unstructured":"Curien P.-L. & Munch-Maccagnoni G. (2010) The duality of computation under focus. In IFIP International Conference on Theoretical Computer Science. Springer Berlin Heidelberg, pp. 165\u2013181."},{"key":"S095679681700003X_ref8","unstructured":"Downen P. & Ariola Z. M. (2014) The duality of construction. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014. Shao, Z. (ed), Lecture Notes in Computer Science, vol. 8410. Springer, Berlin, Heidelberg, pp. 249\u2013269."},{"key":"S095679681700003X_ref7","doi-asserted-by":"publisher","DOI":"10.2307\/2694930"},{"key":"S095679681700003X_ref25","unstructured":"Zeilberger N. (2009) The Logical Basis of Evaluation Order and Pattern-Matching. PhD Thesis, Carnegie Mellon University, Pittsburgh, PA, USA."},{"key":"S095679681700003X_ref2","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"S095679681700003X_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44904-3_9"},{"key":"S095679681700003X_ref16","doi-asserted-by":"crossref","unstructured":"Munch-Maccagnoni G. & Scherer G. (2015) Polarised intermediate representation of lambda calculus with sums. In Proceedings of the 2015 30th Annual ACM\/IEEE Symposium on Logic in Computer Science. LICS '15. Washington, DC, USA: IEEE Computer Society, pp. 127\u2013140.","DOI":"10.1109\/LICS.2015.22"},{"key":"S095679681700003X_ref12","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2947"},{"key":"S095679681700003X_ref10","unstructured":"Herbelin H. (2005) C'est maintenant qu'on calcule : Au c\u0153ur de la dualit\u00e9. Habilitation \u00e0 diriger les reserches, Universit\u00e9 Paris 11."},{"key":"S095679681700003X_ref11","doi-asserted-by":"crossref","unstructured":"Herbelin H. & Ghilezan S. (2008) An approach to call-by-name delimited continuations. In Proceedings of the 35th Annual ACM Sigplan-Sigact Symposium on Principles of Programming Languages. POPL '08. New York, NY, USA: ACM, pp. 383\u2013394.","DOI":"10.1145\/1328438.1328484"},{"key":"S095679681700003X_ref18","doi-asserted-by":"crossref","unstructured":"Parigot M. (1992) Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In Proceedings of the International Conference on Logic Programming and Automated Reasoning. ACM, London, UK, UK: Springer-Verlag, pp. 190\u2013201.","DOI":"10.1007\/BFb0013061"},{"key":"S095679681700003X_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0413-8_5"},{"key":"S095679681700003X_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/1805950.1805958"},{"key":"S095679681700003X_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679681700003X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,22]],"date-time":"2023-08-22T11:09:34Z","timestamp":1692702574000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679681700003X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":25,"alternative-id":["S095679681700003X"],"URL":"https:\/\/doi.org\/10.1017\/s095679681700003x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"article-number":"e12"}}