{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T07:23:37Z","timestamp":1761809017053,"version":"build-2065373602"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T00:00:00Z","timestamp":1761782400000},"content-version":"unspecified","delay-in-days":302,"URL":"https:\/\/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":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We show that recent approaches to quantitative analysis based on non-idempotent typing systems can be extended to programming languages with effects. In particular, we consider two cases: the weak open call-by-name (CBN) and call-by-value (CBV) variants of the\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129525100285_inline1.png\"\/>\n                        <jats:tex-math>$\\lambda$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -calculus, equipped with operations to write and read from a global state. In order to capture quantitative information with respect to time and space for both CBN and CBV, we design for each of them a quantitative type system based on a (tight) multi-type system. One key observation of this work is how CBN and CBV influence the composition of state types. That is, each type system is developed by taking into account how each language manages the global state: in CBN, the composition of state types is almost straightforward, since function application does not require evaluation of its argument; in CBV, however, the interaction between functions and arguments makes the composition of state types more subtle since only values can be passed as actual arguments. The main contribution of this paper is the design of type systems capturing quantitative information about effectful CBN and CBV programming languages. Indeed, we develop type systems that are qualitatively and quantitatively sound and complete.\n                  <\/jats:p>","DOI":"10.1017\/s0960129525100285","type":"journal-article","created":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T07:20:31Z","timestamp":1761808831000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["A quantitative approach to global state composition"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8840-5587","authenticated-orcid":false,"given":"Sandra","family":"Alves","sequence":"first","affiliation":[{"name":"Universidade do Porto"},{"name":"CRACS, INESC-TEC, DCC"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Cit\u00e9"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1211-4270","authenticated-orcid":false,"given":"Miguel","family":"Ramos","sequence":"additional","affiliation":[{"name":"Universidade do Porto"},{"name":"Universit\u00e9 Paris Cit\u00e9"},{"name":"LIACC, DCC"}]}],"member":"56","published-online":{"date-parts":[[2025,10,30]]},"reference":[{"key":"S0960129525100285_ref33","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"S0960129525100285_ref38","unstructured":"Kesner, D. , Peyrot, L. and (FSCD). (2022). Solvability for generalized applications. In: 7th International Conference on Formal Structures for Computation and Deduction, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 18:1\u201318:22."},{"key":"S0960129525100285_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-47963-2_13"},{"key":"S0960129525100285_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002724"},{"key":"S0960129525100285_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_2"},{"key":"S0960129525100285_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/3236789"},{"key":"S0960129525100285_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682000012X"},{"key":"S0960129525100285_ref35","doi-asserted-by":"publisher","DOI":"10.29007\/ggch"},{"key":"S0960129525100285_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"S0960129525100285_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"S0960129525100285_ref37","unstructured":"Kerinec, A. , Manzonetto, G. and Ronchi Della Rocca, S. (2021). Call-by-value, again!, Buenos Aires. In: 6th International Conference on Formal Structures for Computation and Deduction, (FSCD), 2021, Buenos Aires, Argentina (Virtual Conference), Volume 195 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 7:1\u20137:18."},{"key":"S0960129525100285_ref16","doi-asserted-by":"crossref","unstructured":"Bohannon, A. , Pierce, B. C. and Vaughan, J. A. (2006). Relational lenses: a language for updatable views. In: Vansummeren, S. (eds.) Proceedings of the Twenty-Fifth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 26\u201328, 2006, Chicago, Illinois, USA, ACM, 338, 347.","DOI":"10.1145\/1142351.1142399"},{"key":"S0960129525100285_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3479394.3479400"},{"key":"S0960129525100285_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129525100285_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"S0960129525100285_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3434313"},{"key":"S0960129525100285_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-39784-4_4"},{"key":"S0960129525100285_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/363744.363749"},{"key":"S0960129525100285_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"S0960129525100285_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.003"},{"key":"S0960129525100285_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3290320"},{"key":"S0960129525100285_ref28","doi-asserted-by":"crossref","unstructured":"Dezani-Ciancaglini, M. , Giannini, P. and Ronchi Della Rocca, S. (2009). Intersection, universally quantified, and reference types, Coimbra, Portugal. In: 18th Annual Conference of the EACSL on Computer Science Logic, 23rd International Workshop, (CSL), 2009, Coimbra, Portugal. Proceedings, Volume 5771 of Lecture Notes in Computer Science, Springer, 209\u2013224.","DOI":"10.1007\/978-3-642-04027-6_17"},{"key":"S0960129525100285_ref44","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2019-1862"},{"key":"S0960129525100285_ref49","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.018"},{"key":"S0960129525100285_ref10","first-page":"3:1","volume-title":"25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11\u201314, 2019, Oslo, Norway, volume 175 of LIPIcs","author":"Alves","year":"2019"},{"key":"S0960129525100285_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_115"},{"key":"S0960129525100285_ref3","doi-asserted-by":"crossref","unstructured":"Accattoli, B. and Guerrieri, G. (2016). Open call-by-value, Hanoi. In: Igarashi, A. (eds.) Programming Languages and Systems \u2013 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21\u201323, 2016, Proceedings, Volume 10017 of Lecture Notes in Computer Science, 206\u2013226.","DOI":"10.1007\/978-3-319-47958-3_12"},{"key":"S0960129525100285_ref25","unstructured":"de Carvalho, D. (2007). S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. These de doctorat, Universit\u00e9 Aix-Marseille II"},{"key":"S0960129525100285_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59451-5_2"},{"key":"S0960129525100285_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2023.105047"},{"key":"S0960129525100285_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599447"},{"key":"S0960129525100285_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_3"},{"key":"S0960129525100285_ref29","unstructured":"Ehrhard, T. (2012). Collapsing non-idempotent intersection types, Fontainebleau. In: 26th International Workshop\/21st Annual Conference of the EACSL on Computer Science Logic, (CSL), France 16. 259\u2013273, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik."},{"key":"S0960129525100285_ref40","unstructured":"Kesner, D. and Viso, A. (2022). Encoding tight typing in a unified framework, G\u00f6ttingen, 30th EACSL Annual Conference on Computer Science Logic, (CSL), 2022, G\u00f6ttingen, Germany (Virtual Conference), Volume 216 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 27:1\u201327:20."},{"key":"S0960129525100285_ref45","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"S0960129525100285_ref17","doi-asserted-by":"crossref","unstructured":"Breuvart, F. and Dal Lago, U. (2018). On intersection types and probabilistic lambda calculi. In: Sabel, D. and Thiemann, P. (eds.) Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, (PPDP), 2018, Frankfurt am Main, Germany, ACM, 8:1\u20138:13.","DOI":"10.1145\/3236950.3236968"},{"key":"S0960129525100285_ref50","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269968"},{"key":"S0960129525100285_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59025-3_2"},{"key":"S0960129525100285_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"S0960129525100285_ref15","doi-asserted-by":"crossref","unstructured":"Bohannon, A. , Foster, J. N. , Pierce, B. C. , Pilkiewicz, A. and Schmitt, A. (2008). Boomerang: resourceful lenses for string data. In: Necula, G. C. and Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7\u201312, 2008, ACM, 407\u2013419.","DOI":"10.1145\/1328438.1328487"},{"key":"S0960129525100285_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"S0960129525100285_ref36","doi-asserted-by":"crossref","unstructured":"Jones, S. L. P. and Wadler, P. (1993). Imperative functional programming. In: Conference Record of the Twentieth Annual (ACM) (SIGPLAN-SIGACT) Symposium on Principles of Programming Languages, (POPL), 1993, Charleston, South Carolina, USA, ACM Press, 71\u201384. 1993","DOI":"10.1145\/158511.158524"},{"key":"S0960129525100285_ref13","volume-title":"The Lambda Calculus - Its Syntax and Semantics, Volume 103 of Studies in Logic and the Foundations of Mathematics","author":"Barendregt","year":"1985"},{"key":"S0960129525100285_ref39","first-page":"1","article-title":"Non-idempotent types for classical calculi in natural deduction style","volume":"16","author":"Kesner","year":"2020","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129525100285_ref41","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.3.411"},{"key":"S0960129525100285_ref46","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129525100285_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0960129525100285_ref20","doi-asserted-by":"crossref","unstructured":"Carraro, A. and Guerrieri, G. (2014) A semantical and operational account of call-by-value solvability, Grenoble. In: 17th International Conference on Foundations of Software Science and Computation Structures, (FOSSACS), 2014, Grenoble, France, Volume 8412 of Lecture Notes in Computer Science, Springer, 103\u2013118.","DOI":"10.1007\/978-3-642-54830-7_7"},{"key":"S0960129525100285_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3547652"},{"key":"S0960129525100285_ref8","first-page":"1","volume-title":"19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France, volume 26 of LIPIcs","author":"Ahman","year":"2013"},{"key":"S0960129525100285_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"S0960129525100285_ref30","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785699"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129525100285","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T07:20:41Z","timestamp":1761808841000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129525100285\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":52,"alternative-id":["S0960129525100285"],"URL":"https:\/\/doi.org\/10.1017\/s0960129525100285","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. 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 (https:\/\/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"}],"article-number":"e28"}}