{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T11:38:46Z","timestamp":1761824326955,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,9,6]],"date-time":"2021-09-06T00:00:00Z","timestamp":1630886400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,9,6]]},"DOI":"10.1145\/3479394.3479400","type":"proceedings-article","created":{"date-parts":[[2021,10,7]],"date-time":"2021-10-07T22:23:02Z","timestamp":1633645382000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Intersection types for a \u03bb-calculus with global store"],"prefix":"10.1145","author":[{"given":"Ugo","family":"de'Liguoro","sequence":"first","affiliation":[{"name":"University of Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riccardo","family":"Treglia","sequence":"additional","affiliation":[{"name":"University of Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90065-T"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1044"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"H.\u00a0P. Barendregt W. Dekkers and R. Statman. 2013. Lambda Calculus with Types. Cambridge University Press.  H.\u00a0P. Barendregt W. Dekkers and R. Statman. 2013. Lambda Calculus with Types. Cambridge University Press.","DOI":"10.1017\/CBO9781139032636"},{"volume-title":"APPSEM 2000(Lecture Notes in Computer Science, Vol.\u00a02395)","author":"Benton N.","key":"e_1_3_2_1_5_1","unstructured":"N. Benton , J. Hughes , and E. Moggi . 2002. Monads and Effects. In Applied Semantics, International Summer School , APPSEM 2000(Lecture Notes in Computer Science, Vol.\u00a02395) . Springer, 42\u2013122. https:\/\/doi.org\/10.1007\/3-540-45699-6_2 10.1007\/3-540-45699-6_2 N. Benton, J. Hughes, and E. Moggi. 2002. Monads and Effects. In Applied Semantics, International Summer School, APPSEM 2000(Lecture Notes in Computer Science, Vol.\u00a02395). Springer, 42\u2013122. https:\/\/doi.org\/10.1007\/3-540-45699-6_2"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming","author":"Benton N.","year":"2009","unstructured":"N. Benton , A. Kennedy , L. Beringer , and M. Hofmann . 2009. Relational semantics for effect-based program transformations: higher-order store . In Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming , September 7-9, 2009 , Coimbra, Portugal, Ant\u00f3nio Porto and Francisco\u00a0Javier L\u00f3pez-Fraguas (Eds.). ACM, 301\u2013312. https:\/\/doi.org\/10.1145\/1599410.1599447 10.1145\/1599410.1599447 N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. 2009. Relational semantics for effect-based program transformations: higher-order store. In Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, Ant\u00f3nio Porto and Francisco\u00a0Javier L\u00f3pez-Fraguas (Eds.). ACM, 301\u2013312. https:\/\/doi.org\/10.1145\/1599410.1599447"},{"key":"e_1_3_2_1_7_1","volume-title":"4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings(Lecture Notes in Computer Science, Vol.\u00a04279)","author":"Benton N.","year":"1924","unstructured":"N. Benton , A. Kennedy , M. Hofmann , and L. Beringer . 2006. Reading, Writing and Relations. In Programming Languages and Systems , 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings(Lecture Notes in Computer Science, Vol.\u00a04279) . Springer, 114\u2013130. https:\/\/doi.org\/10.1007\/1 1924 661_7 10.1007\/11924661_7 N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. 2006. Reading, Writing and Relations. In Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings(Lecture Notes in Computer Science, Vol.\u00a04279). Springer, 114\u2013130. https:\/\/doi.org\/10.1007\/11924661_7"},{"key":"e_1_3_2_1_8_1","volume-title":"Method. In 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017","author":"Dal Lago U.","year":"2017","unstructured":"U. Dal Lago , F. Gavazzo , and P.\u00a0 B. Levy . 2017 . Effectful Applicative Bisimilarity: Monads, Relators, and Howe\u2019s Method. In 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017 . IEEE Computer Society, 1\u201312. https:\/\/doi.org\/10.1109\/LICS. 2017.8005117 10.1109\/LICS.2017.8005117 U. Dal Lago, F. Gavazzo, and P.\u00a0B. Levy. 2017. Effectful Applicative Bisimilarity: Monads, Relators, and Howe\u2019s Method. In 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017. IEEE Computer Society, 1\u201312. https:\/\/doi.org\/10.1109\/LICS.2017.8005117"},{"volume-title":"Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900)","author":"Davies R.","key":"e_1_3_2_1_9_1","unstructured":"R. Davies and F. Pfenning . 2000. Intersection types and computational effects . In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900) . ACM, 198\u2013208. https:\/\/doi.org\/10.1145\/351240.351259 10.1145\/351240.351259 R. Davies and F. Pfenning. 2000. Intersection types and computational effects. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900). ACM, 198\u2013208. https:\/\/doi.org\/10.1145\/351240.351259"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2020.09.029"},{"key":"e_1_3_2_1_12_1","volume-title":"de\u2019Liguoro and R. Treglia","author":"U.","year":"2021","unstructured":"U. de\u2019Liguoro and R. Treglia . 2021 . From semantics to types: the case of the imperative \u03bb-calculus. (2021). To appear in Proceedings of MFPS 2021. U. de\u2019Liguoro and R. Treglia. 2021. From semantics to types: the case of the imperative \u03bb-calculus. (2021). To appear in Proceedings of MFPS 2021."},{"key":"e_1_3_2_1_13_1","volume-title":"de\u2019Liguoro and R. Treglia","author":"U.","year":"2021","unstructured":"U. de\u2019Liguoro and R. Treglia . 2021 . Intersection Types for a Computational Lambda-Calculus with Global State . arxiv:2104.01358\u00a0[cs.LO] U. de\u2019Liguoro and R. Treglia. 2021. Intersection Types for a Computational Lambda-Calculus with Global State. arxiv:2104.01358\u00a0[cs.LO]"},{"volume-title":"Reflections on Type Theory, Lambda Calculus, and the Mind","author":"Dezani-Ciancaglini M.","key":"e_1_3_2_1_14_1","unstructured":"M. Dezani-Ciancaglini and S. Ronchi Della\u00a0Rocca . 2007. Intersection and Reference Types . In Reflections on Type Theory, Lambda Calculus, and the Mind . Radboud University Nijmegen , 77\u201386. http:\/\/www.di.unito.it\/~dezani\/papers\/dr.pdf M. Dezani-Ciancaglini and S. Ronchi Della\u00a0Rocca. 2007. Intersection and Reference Types. In Reflections on Type Theory, Lambda Calculus, and the Mind. Radboud University Nijmegen, 77\u201386. http:\/\/www.di.unito.it\/~dezani\/papers\/dr.pdf"},{"key":"e_1_3_2_1_15_1","volume-title":"de\u2019Liguoro, and R. Treglia","author":"Faggian C.","year":"2021","unstructured":"C. Faggian , G. Guerrieri , U. de\u2019Liguoro, and R. Treglia . 2021 . On reduction and normalization in the computational core. CoRR abs\/2104.10267(2021). arxiv:2104.10267https:\/\/arxiv.org\/abs\/2104.10267 C. Faggian, G. Guerrieri, U. de\u2019Liguoro, and R. Treglia. 2021. On reduction and normalization in the computational core. CoRR abs\/2104.10267(2021). arxiv:2104.10267https:\/\/arxiv.org\/abs\/2104.10267"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90069-8"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP 1986","author":"Gifford K.","year":"1986","unstructured":"D.\u00a0 K. Gifford and J.\u00a0 M. Lucassen . 1986 . Integrating Functional and Imperative Programming . In Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP 1986 , August 4-6, 1986, Cambridge, Massachusetts, USA. ACM, 28\u201338. D.\u00a0K. Gifford and J.\u00a0M. Lucassen. 1986. Integrating Functional and Imperative Programming. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP 1986, August 4-6, 1986, Cambridge, Massachusetts, USA. ACM, 28\u201338."},{"key":"e_1_3_2_1_19_1","unstructured":"J.-L Krivine. 1993. Lambda calculus types and models. Ellis Horwood.  J.-L Krivine. 1993. Lambda calculus types and models. Ellis Horwood."},{"key":"#cr-split#-e_1_3_2_1_20_1.1","doi-asserted-by":"crossref","unstructured":"U.\u00a0Dal Lago and F. Gavazzo. 2019. Effectful Normal Form Bisimulation. In Programming Languages and Systems - 28th European Symposium on Programming ESOP 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2019 Prague Czech Republic April 6-11 2019 Proceedings(Lecture Notes in Computer Science Vol.\u00a011423) Lu\u00eds Caires (Ed.). Springer 263-292. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_10 10.1007\/978-3-030-17184-1_10","DOI":"10.1007\/978-3-030-17184-1_10"},{"key":"#cr-split#-e_1_3_2_1_20_1.2","doi-asserted-by":"crossref","unstructured":"U.\u00a0Dal Lago and F. Gavazzo. 2019. Effectful Normal Form Bisimulation. In Programming Languages and Systems - 28th European Symposium on Programming ESOP 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2019 Prague Czech Republic April 6-11 2019 Proceedings(Lecture Notes in Computer Science Vol.\u00a011423) Lu\u00eds Caires (Ed.). Springer 263-292. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_10","DOI":"10.1007\/978-3-030-17184-1_10"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.12.025"},{"volume-title":"Foundations for Programming Languages","author":"Mitchell J.C.","key":"e_1_3_2_1_22_1","unstructured":"J.C. Mitchell . 1996. Foundations for Programming Languages . MIT Press, Cambridge , MA. J.C. Mitchell. 1996. Foundations for Programming Languages. MIT Press, Cambridge, MA."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_25_1","unstructured":"A. Pitts and I. Stark. 1998. Operational Reasoning for Functions With Local State. In In Higher Order Operational Techinques in Semantics. Cambridge University Press 227\u2013273.  A. Pitts and I. Stark. 1998. Operational Reasoning for Functions With Local State. In In Higher Order Operational Techinques in Semantics. Cambridge University Press 227\u2013273."},{"volume-title":"Notions of Computation Determine Monads. In FOSSACS 2002(Lecture Notes in Computer Science, Vol.\u00a02303)","author":"Plotkin D.","key":"e_1_3_2_1_26_1","unstructured":"G.\u00a0 D. Plotkin and J. Power . 2002 . Notions of Computation Determine Monads. In FOSSACS 2002(Lecture Notes in Computer Science, Vol.\u00a02303) . Springer, 342\u2013356. https:\/\/doi.org\/10.1007\/3-540-45931-6_24 10.1007\/3-540-45931-6_24 G.\u00a0D. Plotkin and J. Power. 2002. Notions of Computation Determine Monads. In FOSSACS 2002(Lecture Notes in Computer Science, Vol.\u00a02303). Springer, 342\u2013356. https:\/\/doi.org\/10.1007\/3-540-45931-6_24"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.006"},{"key":"e_1_3_2_1_29_1","volume-title":"An Intrinsic Semantics of Intersection Types. In Electronic Proceedings of 3rd International Workshop Intersection Types and Related Systems(ITRS\u201904)","author":"Reynolds J.C.","year":"2000","unstructured":"J.C. Reynolds . 2000 . An Intrinsic Semantics of Intersection Types. In Electronic Proceedings of 3rd International Workshop Intersection Types and Related Systems(ITRS\u201904) , Turku, Finland. 269\u2013270. J.C. Reynolds. 2000. An Intrinsic Semantics of Intersection Types. In Electronic Proceedings of 3rd International Workshop Intersection Types and Related Systems(ITRS\u201904), Turku, Finland. 269\u2013270."},{"key":"e_1_3_2_1_30_1","volume-title":"5th ACM Conference","author":"Swarup V.","year":"1991","unstructured":"V. Swarup , U.\u00a0 S. Reddy , and E. Ireland . 1991. Assignments for Applicative Languages. In Functional Programming Languages and Computer Architecture , 5th ACM Conference , Cambridge, MA, USA , August 26-30, 1991 , Proceedings(Lecture Notes in Computer Science, Vol.\u00a0523), John Hughes (Ed.). Springer, 192\u2013214. https:\/\/doi.org\/10.1007\/3540543961_10 10.1007\/3540543961_10 V. Swarup, U.\u00a0S. Reddy, and E. Ireland. 1991. Assignments for Applicative Languages. In Functional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings(Lecture Notes in Computer Science, Vol.\u00a0523), John Hughes (Ed.). Springer, 192\u2013214. https:\/\/doi.org\/10.1007\/3540543961_10"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1046"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00073-6"},{"key":"e_1_3_2_1_34_1","volume-title":"The Essence of Functional Programming. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Wadler P.","year":"1992","unstructured":"P. Wadler . 1992 . The Essence of Functional Programming. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , 1992. ACM Press, 1\u201314. https:\/\/doi.org\/10.1145\/143165.143169 10.1145\/143165.143169 P. Wadler. 1992. The Essence of Functional Programming. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1992. ACM Press, 1\u201314. https:\/\/doi.org\/10.1145\/143165.143169"},{"volume-title":"Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques(Lecture Notes in Computer Science, Vol.\u00a0925)","author":"Wadler P.","key":"e_1_3_2_1_35_1","unstructured":"P. Wadler . 1995. Monads for Functional Programming . In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques(Lecture Notes in Computer Science, Vol.\u00a0925) . Springer , 24\u201352. https:\/\/doi.org\/10.1007\/3-540-59451-5_2 10.1007\/3-540-59451-5_2 P. Wadler. 1995. Monads for Functional Programming. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques(Lecture Notes in Computer Science, Vol.\u00a0925). Springer, 24\u201352. https:\/\/doi.org\/10.1007\/3-540-59451-5_2"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601776"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"event":{"name":"PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming","acronym":"PPDP 2021","location":"Tallinn Estonia"},"container-title":["23rd International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479400","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3479394.3479400","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479400"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,6]]},"references-count":36,"alternative-id":["10.1145\/3479394.3479400","10.1145\/3479394"],"URL":"https:\/\/doi.org\/10.1145\/3479394.3479400","relation":{},"subject":[],"published":{"date-parts":[[2021,9,6]]},"assertion":[{"value":"2021-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}