{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:58Z","timestamp":1779836758180,"version":"3.53.1"},"reference-count":70,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2020,5,19]],"date-time":"2020-05-19T00:00:00Z","timestamp":1589846400000},"content-version":"unspecified","delay-in-days":139,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Multi types \u2013 aka non-idempotent intersection types \u2013 have 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. Starting from this observation, we refine and generalise a technique introduced by Bernadet and Graham-Lengrand to provide\n                    <jats:italic>exact<\/jats:italic>\n                    bounds. Our typing judgements carry 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\n                    <jats:italic>\u03bb<\/jats:italic>\n                    -calculus (head, leftmost-outermost, and maximal evaluation) and in the linear substitution calculus (linear head evaluation). 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 \u2013 the only known strategy that evaluates terms to full normal forms and provides a reasonable complexity measure \u2013 and 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.\n                  <\/jats:p>","DOI":"10.1017\/s095679682000012x","type":"journal-article","created":{"date-parts":[[2020,5,19]],"date-time":"2020-05-19T04:57:32Z","timestamp":1589864252000},"source":"Crossref","is-referenced-by-count":17,"title":["Tight typings and split bounds, fully developed"],"prefix":"10.1017","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4944-9944","authenticated-orcid":false,"given":"BENIAMINO","family":"ACCATTOLI","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ST\u00c9PHANE","family":"GRAHAM-LENGRAND","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DELIA","family":"KESNER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,5,19]]},"reference":[{"key":"S095679682000012X_ref70","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27861-0_6"},{"key":"S095679682000012X_ref69","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2750"},{"key":"S095679682000012X_ref68","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_26"},{"key":"S095679682000012X_ref67","doi-asserted-by":"publisher","DOI":"10.2307\/2586625"},{"key":"S095679682000012X_ref66","author":"Sim\u00f5es","year":"2007"},{"key":"S095679682000012X_ref65","unstructured":"Pottinger, G. (1980) A type assignment for the strongly normalizable \u03bb-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Seldin, J. P. & Hindley, J. R. (eds). Academic Press, pp. 561\u2013578."},{"key":"S095679682000012X_ref64","author":"Portillo","year":"2002"},{"key":"S095679682000012X_ref63","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000316"},{"key":"S095679682000012X_ref62","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005064"},{"key":"S095679682000012X_ref60","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.07.035"},{"key":"S095679682000012X_ref57","volume-title":"Lambda-Calculus, Types and Models","author":"Krivine","year":"1993"},{"key":"S095679682000012X_ref56","unstructured":"Klop, J. W. (1980) Combinatory Reduction Systems. PhD thesis. Utrecht University."},{"key":"S095679682000012X_ref55","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.3.411"},{"key":"S095679682000012X_ref54","author":"Kesner","year":"2018"},{"key":"S095679682000012X_ref52","unstructured":"Kesner, D. & Vial, P. (2017) Types as resources for classical natural deduction. In FSCD 2017. LIPIcs, Miller, D. (ed.), vol. 84, Oxford, UK. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 24:1\u201324:17."},{"key":"S095679682000012X_ref51","author":"Kesner","year":"2015"},{"key":"S095679682000012X_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44602-7_23"},{"key":"S095679682000012X_ref59","first-page":"1","article-title":"Polyadic approximations, fibrations and intersection types","volume":"2","author":"Mazza","year":"2018","journal-title":"PACMPL"},{"key":"S095679682000012X_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44602-7_26"},{"key":"S095679682000012X_ref49","unstructured":"Kesner, D. & Conch\u00fair, S. (2008) Milner\u2019s Lambda Calculus with Partial Substitutions. Technical report. Paris 7 University. http:\/\/www.pps.univ-paris-diderot.fr\/~kesner\/papers\/shortpartial.pdf"},{"key":"S095679682000012X_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.008"},{"key":"S095679682000012X_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.07.010"},{"key":"S095679682000012X_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224210"},{"key":"S095679682000012X_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9398-9"},{"key":"S095679682000012X_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"S095679682000012X_ref16","author":"Bernadet","year":"2011"},{"key":"S095679682000012X_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.12.012"},{"key":"S095679682000012X_ref15","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:3)2013"},{"key":"S095679682000012X_ref53","article-title":"Non-idempotent types for classical calculi in natural deduction style","volume":"16","author":"Kesner","year":"2019","journal-title":"Log. Methods Comput. Sci."},{"key":"S095679682000012X_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"S095679682000012X_ref61","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016871"},{"key":"S095679682000012X_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"S095679682000012X_ref22","author":"Carraro","year":"2014"},{"key":"S095679682000012X_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.10.003"},{"key":"S095679682000012X_ref14","unstructured":"Bernadet, A. & Graham-Lengrand, S. (2013a). A Big-Step Operational Semantics via Non-idempotent Intersection Types. Technical report. http:\/\/www.lix.polytechnique.fr\/lengrand\/Work\/Reports\/BigStep.pdf"},{"key":"S095679682000012X_ref24","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"S095679682000012X_ref12","unstructured":"Avanzini, M. & Dal Lago, U. (2017). Automating sized-type inference for complexity analysis. PACMPL 1, ICFP, 43:1\u201343:29."},{"key":"S095679682000012X_ref30","unstructured":"de Carvalho, D. (2009). Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs\/0905.4251, pp. 1\u201336."},{"key":"S095679682000012X_ref41","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S095679682000012X_ref44","author":"Hoffmann","year":"2012"},{"key":"S095679682000012X_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00056-7"},{"key":"S095679682000012X_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35722-0_12"},{"key":"S095679682000012X_ref1","unstructured":"Accattoli, B. (2012) An abstract factorization theorem for explicit substitutions. In RTA\u201912. LIPIcs, Tiwari, A. (ed.), vol. 15, Nagoya, Japan. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 6\u201321."},{"key":"S095679682000012X_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02508-3_3"},{"key":"S095679682000012X_ref11","unstructured":"Alves, S. , Kesner, D. & Ventura, D. (2019). A Quantitative Understanding of Pattern Matching. CoRR abs\/1912.01914.arXiv:1912.01914. http:\/\/arxiv.org\/abs\/1912.01914"},{"key":"S095679682000012X_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.12.010"},{"key":"S095679682000012X_ref5","unstructured":"Accattoli, B. & Dal Lago, U. (2012) On the invariance of the unitary cost model for head reduction. In RTA\u201912. LIPIcs, Tiwari, A. (ed.), vol. 15, Nagoya, Japan. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 22\u201337."},{"key":"S095679682000012X_ref6","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(1:4)2016"},{"key":"S095679682000012X_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_3"},{"key":"S095679682000012X_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968608"},{"key":"S095679682000012X_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_15"},{"key":"S095679682000012X_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_30"},{"key":"S095679682000012X_ref31","unstructured":"de Carvalho, D. (2016) The relational model is injective for multiplicative exponential linear logic. In CSL 2016. LIPIcs, Talbot, J.-M. & Regnier, L. (eds), vol. 62, Marseille, France. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 41:1\u201341:19."},{"key":"S095679682000012X_ref21","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzx018"},{"key":"S095679682000012X_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90025-5"},{"key":"S095679682000012X_ref25","article-title":"Linear dependent types and relative completeness","volume":"8","author":"Dal Lago","year":"2011","journal-title":"Log. Methods Comput. Sci."},{"key":"S095679682000012X_ref36","author":"Dudenhefner","year":"2017"},{"key":"S095679682000012X_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"S095679682000012X_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429090"},{"key":"S095679682000012X_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535886"},{"key":"S095679682000012X_ref28","unstructured":"Danos, V. & Regnier, L. (2004) Head Linear Reduction. Technical report."},{"key":"S095679682000012X_ref29","unstructured":"de Carvalho, D. (2007) S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Th\u00e8se de Doctorat. Universit\u00e9 Aix-Marseille II."},{"key":"S095679682000012X_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.017"},{"key":"S095679682000012X_ref37","unstructured":"Ehrhard, T. (2012) Collapsing non-idempotent intersection types. In CSL\u201912. LIPIcs, C\u00e9gielski, P. & Durand, A. (eds.), vol. 16, Fontainebleau, France. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 259\u2013273."},{"key":"S095679682000012X_ref39","author":"Gardner","year":"1994"},{"key":"S095679682000012X_ref58","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90263-1"},{"key":"S095679682000012X_ref42","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.288.1"},{"key":"S095679682000012X_ref43","unstructured":"Guerrieri, G. , Pellissier, L. and Tortora de Falco, L. (2016) Computing connected proof(-structure)s from their Taylor expansion. In FSCD 2016. LIPIcs, Kesner, D. & Pientka, B. (eds), vol. 52, Porto, Portugal. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 20:1\u201320:18."},{"key":"S095679682000012X_ref7","article-title":"Tight typings and split bounds","volume":"2","author":"Accattoli","year":"2018","journal-title":"PACMPL"},{"key":"S095679682000012X_ref45","unstructured":"Hoffmann, J. & Hofmann, M. (2010) Amortized resource analysis with polynomial potential - a static inference of polynomial bounds for functional programs. In ESOP\u201910. Lecture Notes in Computer Science, Gordon, A. D. (ed.), vol. 6012, Paphos, Cyprus. Springer, pp. 287\u2013306."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679682000012X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:51Z","timestamp":1779835011000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679682000012X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":70,"alternative-id":["S095679682000012X"],"URL":"https:\/\/doi.org\/10.1017\/s095679682000012x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"article-number":"e14"}}