{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:56Z","timestamp":1776316916692,"version":"3.50.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["GA 818616"],"award-info":[{"award-number":["GA 818616"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the \u03bb-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provide a new system of multi types (a variant of intersection types) and extract from multi type derivations the space used by the Space KAM, capturing into a type system the space complexity of the abstract machine. Additionally, we show how to capture also the time of the Space KAM, which is a reasonable time cost model, via minor changes to the type system.<\/jats:p>","DOI":"10.1145\/3547650","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"799-825","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Multi types and reasonable space"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4944-9944","authenticated-orcid":false,"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[{"name":"Inria, France \/ \u00c9cole Polytechnique, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8762-8674","authenticated-orcid":false,"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.10.003"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628154"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.01.003"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(1:4)2016"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414108"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434332"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470726"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533362"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236789"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682000012X"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_3"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_15"},{"key":"e_1_2_1_14_1","volume-title":"Ugo Dal Lago, and Gabriele Vanoni","author":"Accattoli Beniamino","year":"2022","unstructured":"Beniamino Accattoli , Ugo Dal Lago, and Gabriele Vanoni . 2022 . Multi Types and Reasonable Space (Long Version). CoRR , https:\/\/doi.org\/10.48550\/arXiv.2207.08795 Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2022. Multi Types and Reasonable Space (Long Version). CoRR, https:\/\/doi.org\/10.48550\/arXiv.2207.08795"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2019.3"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:3)2013"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224210"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394733"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00056-7"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59025-3_2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzx018"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434313"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561456"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00049-3"},{"key":"e_1_2_1_26_1","unstructured":"Daniel de Carvalho. 2007. S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Universit\u00e9 Aix-MarseilleII. \t\t\t\t  Daniel de Carvalho. 2007. S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Universit\u00e9 Aix-MarseilleII."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.017"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22348-9_6"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371095"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9014-0"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_18"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394774"},{"key":"e_1_2_1_37_1","first-page":"1","article-title":"Encoding Tight Typing in a Unified Framework. In CSL (LIPIcs, Vol. 216)","volume":"27","author":"Kesner Delia","year":"2022","unstructured":"Delia Kesner and Andr\u00e9s Viso . 2022 . Encoding Tight Typing in a Unified Framework. In CSL (LIPIcs, Vol. 216) . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 27 : 1 \u2013 27 :20. Delia Kesner and Andr\u00e9s Viso. 2022. Encoding Tight Typing in a Unified Framework. In CSL (LIPIcs, Vol. 216). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 27:1\u201327:20.","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.09.004"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199483"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016871"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012959600223X"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36377-7_4"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002712"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90052-1"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90297-S"},{"key":"e_1_2_1_47_1","volume-title":"Handbook of Theoretical Computer Science","author":"van Emde Boas Peter","unstructured":"Peter van Emde Boas . 1990. Machine Models and Simulation . In Handbook of Theoretical Computer Science , Volume A: Algorithms and Complexity (A). Elsevier and MIT Press, 1\u2013 66 . Peter van Emde Boas. 1990. Machine Models and Simulation. In Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity (A). Elsevier and MIT Press, 1\u201366."},{"key":"e_1_2_1_48_1","volume-title":"Infinitary intersection types as sequences: A new answer to Klop\u2019s problem","author":"Vial Pierre","unstructured":"Pierre Vial . 2017. Infinitary intersection types as sequences: A new answer to Klop\u2019s problem . In LICS. IEEE Computer Society , 1\u201312. Pierre Vial. 2017. Infinitary intersection types as sequences: A new answer to Klop\u2019s problem. In LICS. IEEE Computer Society, 1\u201312."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9019-8"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547650","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547650","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547650"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":49,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547650"],"URL":"https:\/\/doi.org\/10.1145\/3547650","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}