{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T06:19:33Z","timestamp":1790835573070,"version":"4.1.0"},"reference-count":102,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T00:00:00Z","timestamp":1647302400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper is meant to be a survey about implicit characterizations of complexity classes by fragments of higher-order programming languages, with a special focus on type systems and subsystems of linear logic. Particular emphasis will be put on Martin Hofmann\u2019s contributions to the subject, which very much helped in shaping the field.<\/jats:p>","DOI":"10.1017\/s0960129521000505","type":"journal-article","created":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T11:58:52Z","timestamp":1647345532000},"page":"760-776","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Implicit computation complexity in higher-order programming languages"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"U.","family":"Dal Lago","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2022,3,15]]},"reference":[{"key":"S0960129521000505_ref25","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"S0960129521000505_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.05.001"},{"key":"S0960129521000505_ref61","doi-asserted-by":"publisher","DOI":"10.1145\/346048.346051"},{"key":"S0960129521000505_ref78","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005688"},{"key":"S0960129521000505_ref47","doi-asserted-by":"crossref","unstructured":"Gaboardi, M. and Ronchi Della Rocca, S. (2007). A soft type assignment system for lambda -calculus. In: Proceedings of CSL 2007, LNCS, vol. 4646, Springer, 253\u2013267.","DOI":"10.1007\/978-3-540-74915-8_21"},{"key":"S0960129521000505_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.10.005"},{"key":"S0960129521000505_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_4"},{"key":"S0960129521000505_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.09.015"},{"key":"S0960129521000505_ref21","volume-title":"Bounded Arithmetic","author":"Buss","year":"1986"},{"key":"S0960129521000505_ref49","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129521000505_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000632"},{"key":"S0960129521000505_ref53","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0960129521000505_ref34","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(4:7)2010"},{"key":"S0960129521000505_ref82","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.02.010"},{"key":"S0960129521000505_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-009-9210-x"},{"key":"S0960129521000505_ref95","volume-title":"Lectures on the Curry-Howard Isomorphism,","author":"S\u00d8rensen","year":"2006"},{"key":"S0960129521000505_ref83","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1998.743523"},{"key":"S0960129521000505_ref65","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00009-9"},{"key":"S0960129521000505_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.045"},{"key":"S0960129521000505_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00010-5"},{"key":"S0960129521000505_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2159531.2159540"},{"key":"S0960129521000505_ref67","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"S0960129521000505_ref23","author":"Cobham","year":"1965"},{"key":"S0960129521000505_ref37","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000310"},{"key":"S0960129521000505_ref69","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.37"},{"key":"S0960129521000505_ref4","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705666"},{"key":"S0960129521000505_ref97","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319612"},{"key":"S0960129521000505_ref85","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_21"},{"key":"S0960129521000505_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.07.010"},{"key":"S0960129521000505_ref52","first-page":"221","article-title":"Geometry of interaction I: An interpretation of system F","volume":"127","author":"Girard","year":"1988","journal-title":"Logic Colloquium"},{"key":"S0960129521000505_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784759"},{"key":"S0960129521000505_ref41","doi-asserted-by":"crossref","unstructured":"Dal Lago, U. and Sch\u00d6pp, U. (2010). Functional programming in sublinear space. In: Proceedings of ESOP 2010, LNCS, vol. 6012, Springer, 205\u2013225.","DOI":"10.1007\/978-3-642-11957-6_12"},{"key":"S0960129521000505_ref98","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-007-0042-6"},{"key":"S0960129521000505_ref70","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158659"},{"key":"S0960129521000505_ref100","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90019-E"},{"key":"S0960129521000505_ref102","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_29"},{"key":"S0960129521000505_ref94","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.45"},{"key":"S0960129521000505_ref58","doi-asserted-by":"publisher","DOI":"10.2307\/421100"},{"key":"S0960129521000505_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.08.005"},{"key":"S0960129521000505_ref63","first-page":"258","article-title":"A type system for bounded space and functional in-place update","volume":"7","author":"Hofmann","year":"2000","journal-title":"Nordic Journal of Computing"},{"key":"S0960129521000505_ref90","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72734-7_33"},{"key":"S0960129521000505_ref74","unstructured":"Leivant, D. (2002). Calibrating computational feasibility by abstraction rank. In: Proceedings of LICS 2002, IEEE Computer Society, 345."},{"key":"S0960129521000505_ref79","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_26"},{"key":"S0960129521000505_ref42","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.04.006"},{"key":"S0960129521000505_ref88","doi-asserted-by":"publisher","DOI":"10.2307\/2269958"},{"key":"S0960129521000505_ref71","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1998.743522"},{"key":"S0960129521000505_ref31","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005421"},{"key":"S0960129521000505_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/322358.322370"},{"key":"S0960129521000505_ref76","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005131"},{"key":"S0960129521000505_ref80","unstructured":"Mazza, D. (2015). Simple parsimonious types and logarithmic space. In: Proceedings of CSL 2015, LIPIcs, 24\u201340."},{"key":"S0960129521000505_ref81","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_28"},{"key":"S0960129521000505_ref51","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"S0960129521000505_ref15","first-page":"1","article-title":"Elementary complexity and geometry of interaction","volume":"45","author":"Baillot","year":"2001","journal-title":"Fundamenta Informaticae"},{"key":"S0960129521000505_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504081"},{"key":"S0960129521000505_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1131313.1131315"},{"key":"S0960129521000505_ref30","doi-asserted-by":"crossref","unstructured":"Dal Lago, U. (2016). Infinitary lambda calculi from a linear perspective. In: Proceedings of LICS 2016, ACM, 447\u2013456.","DOI":"10.1145\/2933575.2934505"},{"key":"S0960129521000505_ref55","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90363-K"},{"key":"S0960129521000505_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90044-E"},{"key":"S0960129521000505_ref50","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"S0960129521000505_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1555746.1555749"},{"key":"S0960129521000505_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1462179.1462180"},{"key":"S0960129521000505_ref33","first-page":"1","article-title":"Linear dependent types and relative completeness","volume":"8","author":"Dal Lago","year":"2011","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129521000505_ref56","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804106"},{"key":"S0960129521000505_ref7","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(4:10)2007"},{"key":"S0960129521000505_ref68","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.018"},{"key":"S0960129521000505_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.023"},{"key":"S0960129521000505_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.015"},{"key":"S0960129521000505_ref39","doi-asserted-by":"crossref","unstructured":"Dal Lago, U. and Petit, B. (2013). The geometry of types. In: Proceedings of POPL 2013, ACM, 167\u2013178.","DOI":"10.1145\/2480359.2429090"},{"key":"S0960129521000505_ref59","doi-asserted-by":"crossref","unstructured":"Hofmann, M. (1997b). A mixed modal\/linear lambda calculus with applications to bellantoni-cook safe recursion. In: Proceedings of CSL 1997, LNCS, vol. 1414, Springer, 275\u2013294.","DOI":"10.1007\/BFb0028020"},{"key":"S0960129521000505_ref64","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503297"},{"key":"S0960129521000505_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35608-2_31"},{"key":"S0960129521000505_ref72","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_7"},{"key":"S0960129521000505_ref84","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.017"},{"key":"S0960129521000505_ref60","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782641"},{"key":"S0960129521000505_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03816-7_30"},{"key":"S0960129521000505_ref93","doi-asserted-by":"crossref","unstructured":"Roversi, L. (1999). A PTIME completeness proof for light logics. In: Proceedings of CSL 1999, LNCS, vol. 1683, Springer, 469\u2013483.","DOI":"10.1007\/3-540-48168-0_33"},{"key":"S0960129521000505_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090"},{"key":"S0960129521000505_ref99","unstructured":"Terui, K. (2012). Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In: Proceedings of RTA 2012, LIPIcs, 323\u2013338."},{"key":"S0960129521000505_ref57","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1965-0170805-7"},{"key":"S0960129521000505_ref73","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00040-2"},{"key":"S0960129521000505_ref101","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90019-I"},{"key":"S0960129521000505_ref75","doi-asserted-by":"crossref","unstructured":"Leivant, D. and Marion, J. (1994). Ramified recurrence and computational complexity II: Substitution and poly-space. In: Proceedings of CSL 1994, LNCS, vol. 933, Springer, 486\u2013500.","DOI":"10.1007\/BFb0022277"},{"key":"S0960129521000505_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90062-K"},{"key":"S0960129521000505_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983504"},{"key":"S0960129521000505_ref66","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.019"},{"key":"S0960129521000505_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2018.05.003"},{"key":"S0960129521000505_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22177-9_24"},{"key":"S0960129521000505_ref91","unstructured":"Redmond, B. F. (2015). Polynomial time in the parametric lambda calculus. In: Proceedings of TLCA 2015, LIPIcs, vol. 38, 288\u2013301."},{"key":"S0960129521000505_ref26","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:5)2008"},{"key":"S0960129521000505_ref77","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45208-9_4"},{"key":"S0960129521000505_ref92","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.12.013"},{"key":"S0960129521000505_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.10.002"},{"key":"S0960129521000505_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201998"},{"key":"S0960129521000505_ref96","doi-asserted-by":"publisher","DOI":"10.1023\/B:STUD.0000034183.33333.6f"},{"key":"S0960129521000505_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.025"},{"key":"S0960129521000505_ref18","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1190150032"},{"key":"S0960129521000505_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00006-3"},{"key":"S0960129521000505_ref89","unstructured":"Pitt, F. (1994). The Bounded Linear Calculus: A Characterization of the Class of Polynomial-Time Computable Functions Based on Bounded Linear Logic. Master\u2019s thesis, University of Toronto, Department of Computer Science."},{"key":"S0960129521000505_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.10.006"},{"key":"S0960129521000505_ref62","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00010-5"},{"key":"S0960129521000505_ref87","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.01.010"},{"key":"S0960129521000505_ref86","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200610056"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T09:49:23Z","timestamp":1678268963000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000505\/type\/journal_article"}},"subtitle":["A Survey in Memory of Martin Hofmann"],"short-title":[],"issued":{"date-parts":[[2022,3,15]]},"references-count":102,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["S0960129521000505"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000505","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,15]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}