{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,23]],"date-time":"2026-09-23T21:21:13Z","timestamp":1790198473312,"version":"4.1.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T00:00:00Z","timestamp":1503964800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["14CE250005 ELICA and 12IS02001 PACE"],"award-info":[{"award-number":["14CE250005 ELICA and 12IS02001 PACE"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["J-3563"],"award-info":[{"award-number":["J-3563"]}],"id":[{"id":"10.13039\/501100002428","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":[[2017,8,29]]},"abstract":"<jats:p>This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available.<\/jats:p>","DOI":"10.1145\/3110287","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Automating sized-type inference for complexity analysis"],"prefix":"10.1145","volume":"1","author":[{"given":"Martin","family":"Avanzini","sequence":"first","affiliation":[{"name":"University of Innsbruck, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000022"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_15"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"E. Albert S. Genaim and A. N. Masud. 2013. On the Inference of Resource Usage Upper and Lower Bounds. TOCL 14 3 (2013) 22(1\u201335).  E. Albert S. Genaim and A. N. Masud. 2013. On the Inference of Resource Usage Upper and Lower Bounds. TOCL 14 3 (2013) 22(1\u201335).","DOI":"10.1145\/2499937.2499943"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.003"},{"key":"e_1_2_1_5_1","volume-title":"echnical Report). CoRR cs\/CC\/1706.09169","author":"Avanzini M.","year":"2017"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_2_1_7_1","volume-title":"Proc. of 21 st RTA (LIPIcs)","volume":"6","author":"Avanzini M."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_24"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_35"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_11"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02930-1_14"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429090"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.07.010"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_33"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70590-1_8"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837646"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_6"},{"key":"e_1_2_1_25_1","first-page":"e17","article-title":"Type-based Amortized Resource Analysis with Integers and Arrays","volume":"25","author":"Hoffmann J.","year":"2015","journal-title":"JFP"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_1_27_1","volume-title":"Proc. of 37 th POPL. ACM","author":"Jost S.","year":"2010"},{"key":"e_1_2_1_28_1","volume-title":"Proc. of 14 th TACAS (LNCS)","volume":"4963","author":"de Moura L. Mendon\u00e7a"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12925-1_41"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"C. Okasaki. 1999. Purely Functional Data Structures. Cambridge University Press Oxford UK.  C. Okasaki. 1999. Purely Functional Data Structures. Cambridge University Press Oxford UK.","DOI":"10.1017\/CBO9780511530104"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.11.003"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(2:10)2009"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_2_1_36_1","unstructured":"P. Vasconcelos. 2008. Space Cost Analysis Using Sized Types. Ph.D. Dissertation. School of Computer Science University of St Andrews.  P. Vasconcelos. 2008. Space Cost Analysis Using Sized Types. Ph.D. Dissertation. School of Computer Science University of St Andrews."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_27"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110287","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110287","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110287"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":38,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110287"],"URL":"https:\/\/doi.org\/10.1145\/3110287","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,29]]},"assertion":[{"value":"2017-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}