{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T03:26:46Z","timestamp":1781839606081,"version":"3.54.5"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,7,30]]},"abstract":"<jats:p>\n            Multi types\u2014aka non-idempotent intersection types\u2014have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps\n            <jats:italic>and<\/jats:italic>\n            the size of the result. Recent results show that the number of steps can be taken as a reasonable time complexity measure. At the same time, however, these results suggest that multi types provide quite lax complexity bounds, because the size of the result can be exponentially bigger than the number of steps.\n          <\/jats:p>\n          <jats:p>\n            Starting from this observation, we refine and generalise a technique introduced by Bernadet &amp; Graham-Lengrand to provide\n            <jats:italic>exact<\/jats:italic>\n            bounds for the maximal strategy. Our typing judgements carry two counters, one measuring evaluation lengths and the other measuring result sizes. In order to emphasise the modularity of the approach, we provide exact bounds for four evaluation strategies, both in the \u03bb-calculus (head, leftmost-outermost, and maximal evaluation) and in the linear substitution calculus (linear head evaluation).\n          <\/jats:p>\n          <jats:p>Our work aims at both capturing the results in the literature and extending them with new outcomes. Concerning the literature, it unifies de Carvalho and Bernadet &amp; Graham-Lengrand via a uniform technique and a complexity-based perspective. The two main novelties are exact split bounds for the leftmost strategy\u2014the only known strategy that evaluates terms to full normal forms and provides a reasonable complexity measure\u2014and the observation that the computing device hidden behind multi types is the notion of substitution at a distance, as implemented by the linear substitution calculus.<\/jats:p>","DOI":"10.1145\/3236789","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-30","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Tight typings and split bounds"],"prefix":"10.1145","volume":"2","author":[{"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[{"name":"Inria, France \/ \u00c9cole Polytechnique, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"St\u00e9phane","family":"Graham-Lengrand","sequence":"additional","affiliation":[{"name":"CNRS, France \/ Inria, France \/ \u00c9cole Polytechnique, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[{"name":"CNRS, France \/ University of Paris Diderot, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Ashish Tiwari (Ed.)","volume":"15","author":"Accattoli Beniamino","year":"2012","unstructured":"Beniamino Accattoli . 2012 . An Abstract Factorization Theorem for Explicit Substitutions. In RTA\u201912 (LIPIcs) , Ashish Tiwari (Ed.) , Vol. 15 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 6\u201321. Beniamino Accattoli. 2012. An Abstract Factorization Theorem for Explicit Substitutions. In RTA\u201912 (LIPIcs), Ashish Tiwari (Ed.), Vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 6\u201321."},{"key":"e_1_2_2_2_1","volume-title":"Invited paper at LSFA","author":"Accattoli Beniamino","year":"2017","unstructured":"Beniamino Accattoli . 2018. (In) Efficiency and Reasonable Cost Models . Invited paper at LSFA 2017 , to appear. (2018). Beniamino Accattoli. 2018. (In)Efficiency and Reasonable Cost Models. Invited paper at LSFA 2017, to appear. (2018)."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535886"},{"key":"e_1_2_2_4_1","volume-title":"Ashish Tiwari (Ed.)","volume":"15","author":"Accattoli Beniamino","year":"2012","unstructured":"Beniamino Accattoli and Ugo Dal Lago . 2012 . On the Invariance of the Unitary Cost Model for Head Reduction. In RTA\u201912 (LIPIcs) , Ashish Tiwari (Ed.) , Vol. 15 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 22\u201337. Beniamino Accattoli and Ugo Dal Lago. 2012. On the Invariance of the Unitary Cost Model for Head Reduction. In RTA\u201912 (LIPIcs), Ashish Tiwari (Ed.), Vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 22\u201337."},{"key":"e_1_2_2_5_1","volume-title":"Logical Methods in Computer Science 12, 1","author":"Accattoli Beniamino","year":"2016","unstructured":"Beniamino Accattoli and Ugo Dal Lago . 2016. (Leftmost-Outermost) Beta-Reduction is Invariant , Indeed. Logical Methods in Computer Science 12, 1 ( 2016 ). Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outermost) Beta-Reduction is Invariant, Indeed. Logical Methods in Computer Science 12, 1 (2016)."},{"key":"e_1_2_2_6_1","unstructured":"Beniamino Accattoli St\u00e9phane Graham-Lengrand and Delia Kesner. 2018. Tight Typings and Split Bounds (Long Version). (2018). https:\/\/2.zoppoz.workers.dev:443\/http\/arxiv.org\/abs\/1807.02358  Beniamino Accattoli St\u00e9phane Graham-Lengrand and Delia Kesner. 2018. Tight Typings and Split Bounds (Long Version). (2018). https:\/\/2.zoppoz.workers.dev:443\/http\/arxiv.org\/abs\/1807.02358"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110287"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.12.012"},{"key":"e_1_2_2_10_1","volume-title":"Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science 9, 4","author":"Bernadet Alexis","year":"2013","unstructured":"Alexis Bernadet and St\u00e9phane Graham-Lengrand . 2013b. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science 9, 4 ( 2013 ). Alexis Bernadet and St\u00e9phane Graham-Lengrand. 2013b. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science 9, 4 (2013)."},{"key":"e_1_2_2_11_1","volume-title":"FoSSaCS\u201911 (Lecture Notes in Computer Science)","author":"Bernadet Alexis","unstructured":"Alexis Bernadet and St\u00e9phane Lengrand . 2011. Complexity of Strongly Normalising Lambda-Terms via Non-idempotent Intersection Types . In FoSSaCS\u201911 (Lecture Notes in Computer Science) , Martin Hofmann (Ed.), Vol. 6604 . Springer , 88\u2013107. Alexis Bernadet and St\u00e9phane Lengrand. 2011. Complexity of Strongly Normalising Lambda-Terms via Non-idempotent Intersection Types. In FoSSaCS\u201911 (Lecture Notes in Computer Science), Martin Hofmann (Ed.), Vol. 6604. Springer, 88\u2013107."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224210"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00056-7"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.008"},{"key":"e_1_2_2_15_1","volume-title":"IFIP-TCS\u201914 (Lecture Notes in Computer Science), Josep D\u00edaz","author":"Bucciarelli Antonio","unstructured":"Antonio Bucciarelli , Delia Kesner , and Simona Ronchi Della Rocca . 2014. The Inhabitation Problem for Non-idempotent Intersection Types . In IFIP-TCS\u201914 (Lecture Notes in Computer Science), Josep D\u00edaz , Ivan Lanese, and Davide Sangiorgi (Eds.), Vol. 8705 . Springer , 341\u2013354. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. 2014. The Inhabitation Problem for Non-idempotent Intersection Types. In IFIP-TCS\u201914 (Lecture Notes in Computer Science), Josep D\u00edaz, Ivan Lanese, and Davide Sangiorgi (Eds.), Vol. 8705. Springer, 341\u2013354."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzx018"},{"key":"e_1_2_2_17_1","volume-title":"FoSSaCS 2014 (Lecture Notes in Computer Science)","author":"Carraro Alberto","unstructured":"Alberto Carraro and Giulio Guerrieri . 2014. A Semantical and Operational Account of Call-by-Value Solvability . In FoSSaCS 2014 (Lecture Notes in Computer Science) , Anca Muscholl (Ed.), Vol. 8412 . Springer , 103\u2013118. Alberto Carraro and Giulio Guerrieri. 2014. A Semantical and Operational Account of Call-by-Value Solvability. In FoSSaCS 2014 (Lecture Notes in Computer Science), Anca Muscholl (Ed.), Vol. 8412. Springer, 103\u2013118."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_2_21_1","unstructured":"Daniel de Carvalho. 2007. S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Th\u00e8se de Doctorat. Universit\u00e9 Aix-Marseille II.  Daniel de Carvalho. 2007. S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Th\u00e8se de Doctorat. Universit\u00e9 Aix-Marseille II."},{"key":"e_1_2_2_22_1","volume-title":"Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs\/0905.4251","author":"de Carvalho Daniel","year":"2009","unstructured":"Daniel de Carvalho . 2009. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs\/0905.4251 ( 2009 ). Daniel de Carvalho. 2009. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs\/0905.4251 (2009)."},{"key":"e_1_2_2_23_1","volume-title":"The Relational Model Is Injective for Multiplicative Exponential Linear Logic. In CSL","volume":"62","author":"de Carvalho Daniel","year":"2016","unstructured":"Daniel de Carvalho . 2016 . The Relational Model Is Injective for Multiplicative Exponential Linear Logic. In CSL 2016, (LIPIcs), Jean-Marc Talbot and Laurent Regnier (Eds.) , Vol. 62 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 41:1\u201341:19. Daniel de Carvalho. 2016. The Relational Model Is Injective for Multiplicative Exponential Linear Logic. In CSL 2016, (LIPIcs), Jean-Marc Talbot and Laurent Regnier (Eds.), Vol. 62. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 41:1\u201341:19."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.017"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.12.010"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35722-0_12"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009862"},{"key":"e_1_2_2_28_1","volume-title":"Patrick C\u00e9gielski and Arnaud Durand (Eds.)","volume":"16","author":"Ehrhard Thomas","year":"2012","unstructured":"Thomas Ehrhard . 2012 . Collapsing non-idempotent intersection types. In CSL\u201912 (LIPIcs) , Patrick C\u00e9gielski and Arnaud Durand (Eds.) , Vol. 16 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 259\u2013273. Thomas Ehrhard. 2012. Collapsing non-idempotent intersection types. In CSL\u201912 (LIPIcs), Patrick C\u00e9gielski and Arnaud Durand (Eds.), Vol. 16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 259\u2013273."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968608"},{"key":"e_1_2_2_30_1","volume-title":"TACS \u201994 (Lecture Notes in Computer Science), Masami Hagiya and John C","author":"Gardner Philippa","unstructured":"Philippa Gardner . 1994. Discovering Needed Reductions Using Type Theory . In TACS \u201994 (Lecture Notes in Computer Science), Masami Hagiya and John C . Mitchell (Eds.), Vol. 789 . Springer , 555\u2013574. Philippa Gardner. 1994. Discovering Needed Reductions Using Type Theory. In TACS \u201994 (Lecture Notes in Computer Science), Masami Hagiya and John C. Mitchell (Eds.), Vol. 789. Springer, 555\u2013574."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90025-5"},{"key":"e_1_2_2_32_1","volume-title":"Proofs and types","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard , Paul Taylor , and Yves Lafont . 1989. Proofs and types . Cambridge University Press , New York, NY, USA . Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and types. Cambridge University Press, New York, NY, USA."},{"key":"e_1_2_2_33_1","volume-title":"FSCD 2016 (LIPIcs), Delia Kesner and Brigitte Pientka (Eds.)","volume":"52","author":"Guerrieri Giulio","year":"2016","unstructured":"Giulio Guerrieri , Luc Pellissier , and Lorenzo Tortora de Falco . 2016 . Computing Connected Proof(-Structure)s From Their Taylor Expansion . In FSCD 2016 (LIPIcs), Delia Kesner and Brigitte Pientka (Eds.) , Vol. 52 . Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 20:1\u201320:18. Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. 2016. Computing Connected Proof(-Structure)s From Their Taylor Expansion. In FSCD 2016 (LIPIcs), Delia Kesner and Brigitte Pientka (Eds.), Vol. 52. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 20:1\u201320:18."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9398-9"},{"key":"e_1_2_2_39_1","volume-title":"IFIP-TCS\u201914 (Lecture Notes in Computer Science), Josep D\u00edaz","author":"Kesner Delia","unstructured":"Delia Kesner and Daniel Ventura . 2014. Quantitative Types for the Linear Substitution Calculus . In IFIP-TCS\u201914 (Lecture Notes in Computer Science), Josep D\u00edaz , Ivan Lanese, and Davide Sangiorgi (Eds.), Vol. 8705 . Springer , 296\u2013310. Delia Kesner and Daniel Ventura. 2014. Quantitative Types for the Linear Substitution Calculus. In IFIP-TCS\u201914 (Lecture Notes in Computer Science), Josep D\u00edaz, Ivan Lanese, and Davide Sangiorgi (Eds.), Vol. 8705. Springer, 296\u2013310."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25150-9_23"},{"key":"e_1_2_2_41_1","volume-title":"FSCD 2017 (LIPIcs), Dale Miller (Ed.)","volume":"84","author":"Kesner Delia","year":"2017","unstructured":"Delia Kesner and Pierre Vial . 2017 . Types as Resources for Classical Natural Deduction . In FSCD 2017 (LIPIcs), Dale Miller (Ed.) , Vol. 84 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 24:1\u201324:17. Delia Kesner and Pierre Vial. 2017. Types as Resources for Classical Natural Deduction. In FSCD 2017 (LIPIcs), Dale Miller (Ed.), Vol. 84. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 24:1\u201324:17."},{"key":"e_1_2_2_42_1","volume-title":"FoSSaCS\u201918 (Lecture Notes in Computer Science)","author":"Kesner Delia","unstructured":"Delia Kesner , Andr\u00e9s Viso , and Alejandro R\u00edos . 2018. Call-by-need , neededness and all that . In FoSSaCS\u201918 (Lecture Notes in Computer Science) , Christel Baier and Ugo Dal Lago (Eds.), Vol. 10803 . Springer , 241\u2013257. Delia Kesner, Andr\u00e9s Viso, and Alejandro R\u00edos. 2018. Call-by-need, neededness and all that. In FoSSaCS\u201918 (Lecture Notes in Computer Science), Christel Baier and Ugo Dal Lago (Eds.), Vol. 10803. Springer, 241\u2013257."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.3.411"},{"key":"e_1_2_2_45_1","unstructured":"Jean-Louis Krivine. 1993. Lambda-calculus types and models. Ellis Horwood.   Jean-Louis Krivine. 1993. Lambda-calculus types and models. Ellis Horwood."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90263-1"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158094"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.07.035"},{"key":"e_1_2_2_49_1","volume-title":"ICFP","author":"Neergaard Peter M\u00f8ller","year":"2004","unstructured":"Peter M\u00f8ller Neergaard and Harry G. Mairson . 2004. Types, potency, and idempotency: why nonlinearity and amnesia make a type system work . In ICFP 2004 , Chris Okasaki and Kathleen Fisher (Eds.). ACM, 138\u2013149. Peter M\u00f8ller Neergaard and Harry G. Mairson. 2004. Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In ICFP 2004, Chris Okasaki and Kathleen Fisher (Eds.). ACM, 138\u2013149."},{"key":"e_1_2_2_50_1","volume-title":"LICS","author":"Luke Ong C.-H.","year":"2017","unstructured":"C.-H. Luke Ong . 2017 . Quantitative semantics of the lambda calculus: Some generalisations of the relational model . In LICS 2017, Joel Ouaknine (Ed.). IEEE Computer Society, 1\u201312. C.-H. Luke Ong. 2017. Quantitative semantics of the lambda calculus: Some generalisations of the relational model. In LICS 2017, Joel Ouaknine (Ed.). IEEE Computer Society, 1\u201312."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000316"},{"key":"e_1_2_2_52_1","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Pottinger Garrel","unstructured":"Garrel Pottinger . 1980. A Type Assignment for The Strongly Normalizable \u03bb-terms . In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism , J.P. Seldin and J.R. Hindley (Eds.). Academic Press , 561\u2013578. Garrel Pottinger. 1980. A Type Assignment for The Strongly Normalizable \u03bb-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (Eds.). Academic Press, 561\u2013578."},{"key":"e_1_2_2_53_1","volume-title":"Vasconcelos","author":"Sim\u00f5es Hugo R.","year":"2007","unstructured":"Hugo R. Sim\u00f5es , Kevin Hammond , M\u00e1rio Florido , and Pedro B . Vasconcelos . 2007 . Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs. In TYPES 2006, Revised Selected Papers (Lecture Notes in Computer Science), Thorsten Altenkirch and Conor McBride (Eds.), Vol. 4502 . Springer , 221\u2013236. Hugo R. Sim\u00f5es, Kevin Hammond, M\u00e1rio Florido, and Pedro B. Vasconcelos. 2007. Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs. In TYPES 2006, Revised Selected Papers (Lecture Notes in Computer Science), Thorsten Altenkirch and Conor McBride (Eds.), Vol. 4502. Springer, 221\u2013236."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586625"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_26"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2750"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27861-0_6"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/3236789","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/pdf\/10.1145\/3236789","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/3236789"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":54,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236789"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/3236789","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}