{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T22:58:34Z","timestamp":1768345114967,"version":"3.49.0"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T00:00:00Z","timestamp":1673827200000},"content-version":"unspecified","delay-in-days":168,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study the reduction in a <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000433_inline11.png\"\/><jats:tex-math>\n$\\lambda$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-calculus derived from Moggi\u2019s computational one, which we call the computational core. The reduction relation consists of rules obtained by orienting three monadic laws. Such laws, in particular associativity and identity, introduce intricacies in the operational analysis. We investigate the central notions of returning a value versus having a normal form and address the question of normalizing strategies. Our analysis relies on factorization results.<\/jats:p>","DOI":"10.1017\/s0960129522000433","type":"journal-article","created":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T02:19:20Z","timestamp":1673835560000},"page":"934-981","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":6,"title":["On reduction and normalization in the computational core"],"prefix":"10.1017","volume":"32","author":[{"given":"Claudia","family":"Faggian","sequence":"first","affiliation":[]},{"given":"Giulio","family":"Guerrieri","sequence":"additional","affiliation":[]},{"given":"Ugo","family":"de\u2019 Liguoro","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9731-1248","authenticated-orcid":false,"given":"Riccardo","family":"Treglia","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2023,1,16]]},"reference":[{"key":"S0960129522000433_ref42","first-page":"403","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"Scott","year":"1980"},{"key":"S0960129522000433_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_19"},{"key":"S0960129522000433_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"S0960129522000433_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"S0960129522000433_ref23","unstructured":"Guerrieri, G. and Olimpieri, F. (2021). Categorifying non-idempotent intersection types. In: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25\u201328, 2021, Ljubljana, Slovenia (Virtual Conference), LIPIcs, vol. 183, Schloss Dagstuhl, 25:1\u201325:24."},{"key":"S0960129522000433_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_17"},{"key":"S0960129522000433_ref7","unstructured":"Barendregt, H. (1984). The Lambda Calculus: Its Syntax and Semantics, revised edition, Studies in Logic and the Foundations of Mathematics, vol. 103, North-Holland."},{"key":"S0960129522000433_ref31","unstructured":"Leroy, X. (1990). The ZINC experiment: An economical implementation of the ML language. Technical report 117, INRIA."},{"key":"S0960129522000433_ref39","doi-asserted-by":"crossref","DOI":"10.2307\/1968867","article-title":"On theories with a combinatorial definition of equivalence","volume":"43","author":"Newman","year":"1942","journal-title":"Annals of Mathematics"},{"key":"S0960129522000433_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_7"},{"key":"S0960129522000433_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29822-6_4"},{"key":"S0960129522000433_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129522000433_ref16","unstructured":"Ehrhard, T. (2012). Collapsing non-idempotent intersection types. In: Computer Science Logic (CSL\u201912) - 26th International Workshop\/21st Annual Conference of the EACSL, CSL 2012, LIPIcs, vol. 16, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 259\u2013273."},{"key":"S0960129522000433_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59025-3_2"},{"key":"S0960129522000433_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.044"},{"key":"S0960129522000433_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129522000433_ref29","unstructured":"Jones, S. L. P. , Shields, M. , Launchbury, J. and Tolmach, A. P. (1998). Bridging the gulf: A common intermediate language for ML and haskell. In: MacQueen, D. B. and Cardelli, L. (eds.) POPL\u201998, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19\u201321, 1998, ACM, 49\u201361."},{"key":"S0960129522000433_ref4","doi-asserted-by":"crossref","unstructured":"Accattoli, B. and Guerrieri, G. (2016). Open call-by-value. In: Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21\u201323, 2016, Proceedings, Lecture Notes in Computer Science, vol. 10017, 206\u2013226, Springer.","DOI":"10.1007\/978-3-319-47958-3_12"},{"key":"S0960129522000433_ref34","unstructured":"MacLane, S. (1997). Categories for the Working Mathematician, 2nd ed., Graduate Texts in Mathematics, Springer, New York, NY.Please provide publisher location for \u201cMacLane (1997)\u201d."},{"key":"S0960129522000433_ref37","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"S0960129522000433_ref44","volume-title":"Cambridge Tracts in Theoretical Computer Science","volume":"55","year":"2003"},{"key":"S0960129522000433_ref20","unstructured":"Filinski, A. (1996). Controlling Effects. Phd thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania."},{"key":"S0960129522000433_ref35","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0304-3975(98)00358-2","article-title":"Call-by-name, call-by-value, call-by-need and the linear lambda calculus","volume":"228","author":"Maraist","year":"1999","journal-title":"Theoretical Computer Science"},{"key":"S0960129522000433_ref36","unstructured":"Moggi, E. (1988). Computational Lambda-calculus and Monads. Report ECS-LFCS-88-66, University of Edinburgh, Edinburgh, Scotland."},{"key":"S0960129522000433_ref26","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.293.5"},{"key":"S0960129522000433_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968608"},{"key":"S0960129522000433_ref11","unstructured":"Crary, K. (2009). Simple proof of call-by-value standardization. Technical report, Carnegie Mellon University, Computer Science Department. Paper 474."},{"key":"S0960129522000433_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_9"},{"key":"S0960129522000433_ref47","unstructured":"van Oostrom, V. (2020a). Private communication via electronic mail."},{"key":"S0960129522000433_ref12","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"S0960129522000433_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45699-6_2"},{"key":"S0960129522000433_ref48","unstructured":"van Oostrom, V. (2020b). Some symmetries of commutation diamonds. In: Proceedings of the 9th International Workshop on Confluence (IWC 2020), Paris, France, 1\u20135."},{"key":"S0960129522000433_ref49","first-page":"1","volume-title":"Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1992","author":"Wadler","year":"1992"},{"key":"S0960129522000433_ref28","doi-asserted-by":"crossref","unstructured":"Herbelin, H. and Zimmermann, S. (2009). An operational account of call-by-value minimal and classical lambda-calculus in \"natural deduction\" form. In: Curien, P.-L. (ed.) Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009. Proceedings, Lecture Notes in Computer Science, vol. 5608, Springer, 142\u2013156.","DOI":"10.1007\/978-3-642-02273-9_12"},{"key":"S0960129522000433_ref40","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","article-title":"Call-by-name, call-by-value and the lambda-calculus","volume":"1","author":"Plotkin","year":"1975","journal-title":"Theoretical Computer Science"},{"key":"S0960129522000433_ref45","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1016\/0304-3975(92)00023-K","article-title":"Confluence by decreasing diagrams","volume":"126","author":"van Oostrom","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"S0960129522000433_ref13","unstructured":"de\u2019 Liguoro, U. and Treglia, R. (2019). Intersection types for the computational lambda-calculus. CoRR, abs\/1907.05706."},{"key":"S0960129522000433_ref46","doi-asserted-by":"crossref","unstructured":"van Oostrom, V. (2008). Confluence by decreasing diagrams converted. In: Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Lecture Notes in Computer Science, vol. 5117, Springer, 306\u2013320.","DOI":"10.1007\/978-3-540-70590-1_21"},{"key":"S0960129522000433_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269968"},{"key":"S0960129522000433_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2020.09.029"},{"key":"S0960129522000433_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_11"},{"key":"S0960129522000433_ref27","unstructured":"Hindley, J. R. (1964). The Church-Rosser Property and a Result in Combinatory Logic. Phd thesis, University of Newcastle-upon-Tyne."},{"key":"S0960129522000433_ref3","unstructured":"Accattoli, B. , Faggian, C. and Guerrieri, G. (2021). Factorize factorization. In: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25\u201328, 2021, Ljubljana, Slovenia (Virtual Conference), LIPIcs, vol. 183, Schloss Dagstuhl, 6:1\u20136:25."},{"key":"S0960129522000433_ref51","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/601775.601776","article-title":"The marriage of effects and monads","volume":"4","author":"Wadler","year":"2003","journal-title":"ACM Transactions on Computational Logic"},{"key":"S0960129522000433_ref22","doi-asserted-by":"crossref","unstructured":"Guerrieri, G. and Manzonetto, G. (2019). The bang calculus and the two Girard\u2019s translations. In: Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018), EPTCS, vol. 292, 15\u201330.","DOI":"10.4204\/EPTCS.292.2"},{"key":"S0960129522000433_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.08.006"},{"key":"S0960129522000433_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_17"},{"key":"#cr-split#-S0960129522000433_ref24.1","unstructured":"Guerrieri, G. , Paolini, L. and Ronchi Della Rocca, S. (2017). Standardization and conservativity of a refined call-by-value lambda-calculus. Logical Methods in Computer Science 13"},{"key":"#cr-split#-S0960129522000433_ref24.2","unstructured":"(4) 4-29.Please provide page number for \"Guerrieri et al. (2017)\"."},{"key":"S0960129522000433_ref25","unstructured":"Guerrieri, G. (2015). Head reduction and normalization in a call-by-value lambda-calculus. In: 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015, OASICS, vol. 46, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 3\u201317."},{"key":"S0960129522000433_ref6","doi-asserted-by":"crossref","unstructured":"Baader, F. and Nipkow, T. (1998). Term Rewriting and All that, Cambridge University Press, USA.Please provide publisher location for \u201cBaader and Nipkow (1998)\u201d.","DOI":"10.1017\/CBO9781139172752"},{"key":"S0960129522000433_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59451-5_2"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000433","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,22]],"date-time":"2023-02-22T08:15:44Z","timestamp":1677053744000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000433\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8]]},"references-count":52,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["S0960129522000433"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000433","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}