{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:54Z","timestamp":1775873514547,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"AFOSR","doi-asserted-by":"crossref","award":["MURI FA9550-15-1-0053"],"award-info":[{"award-number":["MURI FA9550-15-1-0053"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]},{"name":"NSF","award":["CCF-1901381"],"award-info":[{"award-number":["CCF-1901381"]}]},{"DOI":"10.13039\/100006602","name":"AFRL","doi-asserted-by":"crossref","award":["NDSEG"],"award-info":[{"award-number":["NDSEG"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            We present\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mstyle mathvariant=\"bold\">\n                  <mml:mtext>decalf<\/mml:mtext>\n                <\/mml:mstyle>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , a\n            <jats:bold>d<\/jats:bold>\n            irected,\n            <jats:bold>e<\/jats:bold>\n            ffectful\n            <jats:bold>c<\/jats:bold>\n            ost-\n            <jats:bold>a<\/jats:bold>\n            ware\n            <jats:bold>l<\/jats:bold>\n            ogical\n            <jats:bold>f<\/jats:bold>\n            ramework for studying quantitative aspects of functional programs with effects. Like\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mstyle mathvariant=\"bold\">\n                  <mml:mtext>calf<\/mml:mtext>\n                <\/mml:mstyle>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , the language is based on a formal\n            <jats:italic toggle=\"yes\">phase distinction<\/jats:italic>\n            between the\n            <jats:italic toggle=\"yes\">extension<\/jats:italic>\n            and the\n            <jats:italic toggle=\"yes\">intension<\/jats:italic>\n            of a program, its pure\n            <jats:italic toggle=\"yes\">behavior<\/jats:italic>\n            as distinct from its\n            <jats:italic toggle=\"yes\">cost<\/jats:italic>\n            measured by an effectful step-counting primitive. The type theory ensures that the behavior is unaffected by the cost accounting. Unlike\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mstyle mathvariant=\"bold\">\n                  <mml:mtext>calf<\/mml:mtext>\n                <\/mml:mstyle>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , the present language takes account of\n            <jats:italic toggle=\"yes\">effects<\/jats:italic>\n            , such as probabilistic choice and mutable state. This extension requires a reformulation of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mstyle mathvariant=\"bold\">\n                  <mml:mtext>calf<\/mml:mtext>\n                <\/mml:mstyle>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            \u2019s approach to cost accounting: rather than rely on a \u201cseparable\u201d notion of cost, here\n            <jats:italic toggle=\"yes\">a cost bound is simply another program<\/jats:italic>\n            . To make this formal, we equip every type with an intrinsic preorder, relaxing the precise cost accounting intrinsic to a program to a looser but nevertheless informative estimate. For example, the cost bound of a probabilistic program is itself a probabilistic program that specifies the distribution of costs. This approach serves as a streamlined alternative to the standard method of isolating a cost recurrence and readily extends to higher-order, effectful programs.\n          <\/jats:p>\n          <jats:p>\n            The development proceeds by first introducing the\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mstyle mathvariant=\"bold\">\n                  <mml:mtext>decalf<\/mml:mtext>\n                <\/mml:mstyle>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            type system, which is based on an intrinsic ordering among terms that restricts in the extensional phase to extensional equality, but in the intensional phase reflects an approximation of the cost of a program of interest. This formulation is then applied to a number of illustrative examples, including pure and effectful sorting algorithms, simple probabilistic programs, and higher-order functions. Finally, we justify\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mstyle mathvariant=\"bold\">\n                  <mml:mtext>decalf<\/mml:mtext>\n                <\/mml:mstyle>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            via a model in the topos of augmented simplicial sets.\n          <\/jats:p>","DOI":"10.1145\/3632852","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"273-301","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Decalf: A Directed, Effectful Cost-Aware Logical Framework"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0947-3520","authenticated-orcid":false,"given":"Harrison","family":"Grodin","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4888-6042","authenticated-orcid":false,"given":"Yue","family":"Niu","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0585-5564","authenticated-orcid":false,"given":"Jonathan","family":"Sterling","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9400-2941","authenticated-orcid":false,"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/978-3-662-49630-5_3","volume-title":"Foundations of Software Science and Computation Structures","author":"Ahman Danel","year":"2016","unstructured":"Danel Ahman, Neil Ghani, and Gordon D. Plotkin. 2016. Dependent Types and Fibred Computational Effects. In Foundations of Software Science and Computation Structures, Bart Jacobs and Christof L\u00f6ding (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 36\u201354."},{"key":"e_1_3_1_3_1","volume-title":"Th\u00e9orie des topos et cohomologie \u00e9tale des sch\u00e9mas","author":"Artin Michael","year":"1972","unstructured":"Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier. 1972. Th\u00e9orie des topos et cohomologie \u00e9tale des sch\u00e9mas. Lecture Notes in Mathematics, Vol. 269, 270, 305. Springer-Verlag, Berlin. S\u00e9minaire de G\u00e9om\u00e9trie Alg\u00e9brique du Bois-Marie 1963\u20131964 (SGA 4), Dirig\u00e9 par M. Artin, A. Grothendieck, et J.-L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat."},{"key":"e_1_3_1_4_1","unstructured":"Steve Awodey Nicola Gambino and Sina Hazratpour. 2021. Kripke-Joyal forcing for type theory and uniform fibrations. (2021). arXiv:2110.14576 [math.LO] Unpublished manuscript."},{"key":"e_1_3_1_5_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2022. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https:\/\/iris-project.org\/tutorial-material.html"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2020.01"},{"issue":"3","key":"e_1_3_1_7_1","first-page":"231","article-title":"Sur les mod\u00e8les de la g\u00e9om\u00e9trie diff\u00e9rentielle synth\u00e9tique","volume":"20","author":"Dubuc Eduardo J.","year":"1979","unstructured":"Eduardo J. Dubuc. 1979. Sur les mod\u00e8les de la g\u00e9om\u00e9trie diff\u00e9rentielle synth\u00e9tique. Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques 20, 3 (1979), 231\u2013279. http:\/\/eudml.org\/doc\/91216","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002429"},{"key":"e_1_3_1_9_1","doi-asserted-by":"crossref","unstructured":"Marcelo P. Fiore Andrew M. Pitts and S. C. Steenkamp. 2021. Quotients inductive types and quotient inductive types. (2021). arXiv:2101.02994 [cs.LO]","DOI":"10.46298\/lmcs-18(2:15)2022"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80165-3"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00221-8"},{"key":"e_1_3_1_12_1","unstructured":"Daniel Gratzer and Jonathan Sterling. 2020. Syntactic categories for dependent type theory: sketching and adequacy. (2020). arXiv:2012.10783 [cs.LO] Unpublished manuscript."},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CALCO.2023.23"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Harrison Grodin Robert Harper Yue Niu and Jonathan Sterling. 2023. Decalf: A Directed Effectful Cost-Aware Logical Framework (Extended Version). https:\/\/doi.org\/10.48550\/arXiv.2307.05938 10.48550\/arXiv.2307.05938 arXiv:2307.05938 [cs]","DOI":"10.48550\/arXiv.2307.05938"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Harrison Grodin Yue Niu Jonathan Sterling and Robert Harper. 2024. agda-calf v2.0.0. https:\/\/doi.org\/10.1145\/3580425 10.1145\/3580425","DOI":"10.1145\/3580425"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96744"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/366622.366644"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/5.1.10"},{"key":"e_1_3_1_19_1","volume-title":"Extensional concepts in intensional type theory","author":"Hofmann Martin","year":"1995","unstructured":"Martin Hofmann. 1995. Extensional concepts in intensional type theory. Ph. D. Dissertation. University of Edinburgh, Edinburgh."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084217"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371083"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0954-6"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.026"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004962"},{"key":"e_1_3_1_26_1","first-page":"iv+91","volume":"1","author":"Martin-L\u00f6f Per","year":"1984","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Studies in Proof Theory, Vol. 1. Bibliopolis. iv+91 pages.","journal-title":"Intuitionistic type theory"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498670"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Yue Niu Jonathan Sterling Harrison Grodin and Robert Harper. 2022b. agda-calf. https:\/\/doi.org\/10.1145\/3462303 10.1145\/3462303","DOI":"10.1145\/3462303"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_3_1_31_1","volume-title":"Domain Theory in Realizability Toposes","author":"Phoa Wesley","year":"1991","unstructured":"Wesley Phoa. 1991. Domain Theory in Realizability Toposes. Ph. D. Dissertation. University of Edinburgh."},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704856"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434308"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"e_1_3_1_36_1","volume-title":"Classifying Types","author":"Rijke Egbert","year":"2019","unstructured":"Egbert Rijke. 2019. Classifying Types. Ph. D. Dissertation. Carnegie Mellon University. arXiv:1906.09435"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:2)2020"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6990769"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.31"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(1:43)2022"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"e_1_3_1_42_1","volume-title":"Abstract and Concrete Type Theories","author":"Uemura Taichi","year":"2021","unstructured":"Taichi Uemura. 2021. Abstract and Concrete Type Theories. Ph. D. Dissertation. Universiteit van Amsterdam, Amsterdam. https:\/\/www.illc.uva.nl\/cms\/Research\/Publications\/Dissertations\/DS-2021-09.text.pdf"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000208"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1706.07997"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632852","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632852","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:32Z","timestamp":1751659472000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632852"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632852"],"URL":"https:\/\/doi.org\/10.1145\/3632852","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}