{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:11Z","timestamp":1751660531902,"version":"3.28.0"},"reference-count":37,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,6,29]]},"DOI":"10.1109\/lics52264.2021.9470726","type":"proceedings-article","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T20:14:07Z","timestamp":1625688847000},"page":"1-13","source":"Crossref","is-referenced-by-count":3,"title":["The Space of Interaction"],"prefix":"10.1109","author":[{"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo Dal","family":"Lago","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","first-page":"24","article-title":"Simple parsimonious types and logarithmic space","volume":"41","author":"mazza","year":"2015","journal-title":"24th EACSL Annual Conference on Computer Science Logic CSL 2015"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199483"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"journal-title":"Lambda-calculus types and models","year":"1993","author":"krivine","key":"ref30"},{"key":"ref37","first-page":"215","article-title":"Some unusual ?-calculus numeral systems","author":"wadsworth","year":"1980","journal-title":"To H B Curry Essays on combinatory logic lambda calculus and formalism"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005093"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.45"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3158094"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_15"},{"key":"ref11","first-page":"3:1","article-title":"A quantitative understanding of pattern matching","author":"alves","year":"2019","journal-title":"25th International Conference on Types for Proofs and Programs TYPES 2019"},{"journal-title":"The Lambda Calculus Its Syntax and Semantics","year":"1984","author":"barendregt","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59025-3_2"},{"key":"ref14","first-page":"2208","article-title":"Type systems","author":"cardelli","year":"1997","journal-title":"The Computer Science and Engineering Handbook"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"ref16","article-title":"Encoding turing machines into the deterministic lambda-calculus","volume":"abs 1711 10078","author":"dal lago","year":"2017","journal-title":"CoRR"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3434313","article-title":"Intersection types and (positive) almost-sure termination","volume":"5","author":"dal lago","year":"2021","journal-title":"Proc ACM Program Lang"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_12"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.04.006"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(1:4)2016"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.018"},{"key":"ref3","first-page":"22","article-title":"On the invariance of the unitary cost model for head reduction","volume":"15","author":"accattoli","year":"2012","journal-title":"23rd International Conference on Rewriting Techniques and Applications (RTA&#x2019;12) RTA 2012"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3434332","article-title":"The (in)efficiency of interaction","volume":"5","author":"accattoli","year":"2021","journal-title":"Proc ACM Program Lang"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394774"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414108"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682000012X"},{"key":"ref7","article-title":"The space of interaction","author":"accattoli","year":"2021","journal-title":"Tech Rep"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131855"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_3"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561456"},{"key":"ref22","article-title":"S&#x00E9;mantiques de la logique lin&#x00E9;aire et temps de calcul","author":"de carvalho","year":"2007","journal-title":"Th&#x00E8;se de doctorat"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150.016"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.017"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190269"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3371095"}],"event":{"name":"2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","start":{"date-parts":[[2021,6,29]]},"location":"Rome, Italy","end":{"date-parts":[[2021,7,2]]}},"container-title":["2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9470497\/9470501\/09470726.pdf?arnumber=9470726","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,10]],"date-time":"2022-05-10T15:46:22Z","timestamp":1652197582000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9470726\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,29]]},"references-count":37,"URL":"https:\/\/doi.org\/10.1109\/lics52264.2021.9470726","relation":{},"subject":[],"published":{"date-parts":[[2021,6,29]]}}}