{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:27:26Z","timestamp":1770294446458,"version":"3.49.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1718220,1845803,1801369,1845514,1812876,2007784"],"award-info":[{"award-number":["1718220,1845803,1801369,1845514,1812876,2007784"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-18-C-0092"],"award-info":[{"award-number":["FA8750-18-C-0092"]}],"id":[{"id":"10.13039\/100000185","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":[[2021,1,4]]},"abstract":"<jats:p>This paper presents \u03bb-amor, a new type-theoretic framework for amortized cost analysis of higher-order functional programs and shows that existing type systems for cost analysis can be embedded in it. \u03bb-amor introduces a new modal type for representing potentials \u2013 costs that have been accounted for, but not yet incurred, which are central to amortized analysis. Additionally, \u03bb-amor relies on standard type-theoretic concepts like affineness, refinement types and an indexed cost monad. \u03bb-amor is proved sound using a rather simple logical relation. We embed two existing type systems for cost analysis in \u03bb-amor showing that, despite its simplicity, \u03bb-amor can simulate cost analysis for different evaluation strategies (call-by-name and call-by-value), in different styles (effect-based and coeffect-based), and with or without amortization. One of the embeddings also implies that \u03bb-amor is relatively complete for all terminating PCF programs.<\/jats:p>","DOI":"10.1145\/3434308","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["A unifying type-theory for higher-order (amortized) cost analysis"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7701-8311","authenticated-orcid":false,"given":"Vineet","family":"Rajani","sequence":"first","affiliation":[{"name":"MPI-SP, Germany"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[{"name":"Boston University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0888-3093","authenticated-orcid":false,"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_2_1","volume-title":"Syntax and Semantics of Quantitative Type Theory. In Annual ACM\/IEEE Symposium on Logic in Computer Science.","author":"Atkey Robert","year":"2018","unstructured":"Robert Atkey . 2018 . Syntax and Semantics of Quantitative Type Theory. In Annual ACM\/IEEE Symposium on Logic in Computer Science. Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Annual ACM\/IEEE Symposium on Logic in Computer Science."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110287"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_2_1_8_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , and Cliford Stein . 2009. Introduction to Algorithms , 3 rd Edition. MIT Press . Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Cliford Stein. 2009. Introduction to Algorithms, 3rd Edition. MIT Press.","edition":"3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8 4 ( 2011 ).  Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8 4 ( 2011 ).","DOI":"10.2168\/LMCS-8(4:11)2012"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Ugo Dal Lago and Barbara Petit. 2012. Linear Dependent Types in a Call-by-value Scenario. Science of Computer Programming 84 ( 2012 ).  Ugo Dal Lago and Barbara Petit. 2012. Linear Dependent Types in a Call-by-value Scenario. Science of Computer Programming 84 ( 2012 ).","DOI":"10.1145\/2370776.2370792"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_2_1_15_1","volume-title":"Scott","author":"Girard Jean-Yves","year":"1992","unstructured":"Jean-Yves Girard , Andre Scedrov , and Philip J . Scott . 1992 . Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science 97, 1 ( 1992 ). Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science 97, 1 ( 1992 )."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"e_1_2_1_17_1","volume-title":"Haslbeck and Tobias Nipkow","author":"Maximilian P.","year":"2018","unstructured":"Maximilian P. L. Haslbeck and Tobias Nipkow . 2018 . Hoare Logics for Time Bounds-A Study in Meta Theory. In Tools and Algorithms for the Construction and Analysis of Systems , Vol. 10805 . Maximilian P. L. Haslbeck and Tobias Nipkow. 2018. Hoare Logics for Time Bounds-A Study in Meta Theory. In Tools and Algorithms for the Construction and Analysis of Systems, Vol. 10805."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9398-9"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371083"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314602"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Jean-Louis Krivine. 2007. A Call-by-name Lambda-calculus Machine. Higher Order Symbolic Computation 20 3 ( 2007 ).  Jean-Louis Krivine. 2007. A Call-by-name Lambda-calculus Machine. Higher Order Symbolic Computation 20 3 ( 2007 ).","DOI":"10.1007\/s10990-007-9018-9"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009874"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Dylan McDermott and Alan Mycroft. 2018. Call-by-need efects via coefects. Open Comput. Sci. 8 1 ( 2018 ).  Dylan McDermott and Alan Mycroft. 2018. Call-by-need efects via coefects. Open Comput. Sci. 8 1 ( 2018 ).","DOI":"10.1515\/comp-2018-0009"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Eugenio Moggi. 1991. Notions of Computation and Monads. Information and Computation 93 1 ( 1991 ).  Eugenio Moggi. 1991. Notions of Computation and Monads. Information and Computation 93 1 ( 1991 ).","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000165"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_1_36_1","volume-title":"Coefects: Unified Static Analysis of Context-Dependence. In Automata, Languages, and Programming-International Colloquium.","author":"Petricek Tomas","year":"2013","unstructured":"Tomas Petricek , Dominic A. Orchard , and Alan Mycroft . 2013 . Coefects: Unified Static Analysis of Context-Dependence. In Automata, Languages, and Programming-International Colloquium. Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. 2013. Coefects: Unified Static Analysis of Context-Dependence. In Automata, Languages, and Programming-International Colloquium."},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"David J. Pym Peter W. O'Hearn and Hongseok Yang. 2004. Possible worlds and resources: the semantics of BI. Theoretical Computer Science 315 1 ( 2004 ).  David J. Pym Peter W. O'Hearn and Hongseok Yang. 2004. Possible worlds and resources: the semantics of BI. Theoretical Computer Science 315 1 ( 2004 ).","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434308","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434308","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434308","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434308"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434308"],"URL":"https:\/\/doi.org\/10.1145\/3434308","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}