{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T20:46:23Z","timestamp":1773434783538,"version":"3.50.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/100000181","name":"United States Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-21-0009"],"award-info":[{"award-number":["FA9550-21-0009"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000181","name":"United States Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-23-1-0434"],"award-info":[{"award-number":["FA9550-23-1-0434"]}],"id":[{"id":"10.13039\/100000181","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":[[2026,1,8]]},"abstract":"<jats:p>Software development depends on the use of libraries whose public specifications inform client code and impose obligations on private implementations; it follows that verification at scale must also be modular, preserving such abstraction. Hoare's influential methodology uses abstraction functions to demonstrate the coherence between such concrete implementations and their abstract specifications. However, the Hoare methodology relies on a conventional separation between implementation and specification, providing no linguistic support for ensuring that this convention is obeyed.<\/jats:p>\n                  <jats:p>This paper proposes a synthetic account of Hoare's methodology within univalent dependent type theory by encoding the data of abstraction functions within types themselves. This is achieved via a phase distinction, which gives rise to a gluing construction that renders an abstraction function as a type and a pair of modalities that fracture a type into its concrete and abstract parts. A noninterference theorem governing the phase distinction characterizes the modularity guarantees provided by the theory.<\/jats:p>\n                  <jats:p>This approach scales to verification of cost, allowing the analysis of client cost relative to a cost-aware specification. A monadic sealing effect facilitates modularity of cost, permitting an implementation to be upper-bounded by its specification in cases where private details influence observable cost. The resulting theory supports modular development of programs and proofs in a manner that hides private details of no concern to clients while permitting precise specifications of both the cost and behavior of programs.<\/jats:p>","DOI":"10.1145\/3776673","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"895-922","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory"],"prefix":"10.1145","volume":"10","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-0001-7600-9069","authenticated-orcid":false,"given":"Runming","family":"Li","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}]},{"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":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Blelloch","author":"Acar Umut A.","year":"2022","unstructured":"Umut A. Acar and Guy E. Blelloch. 2022. Algorithms: Parallel and Sequential. http:\/\/www.algorithms-book.com\/"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_3"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434293"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.23"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3512769"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/865063"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2935764.2935768"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(82)90015-1"},{"key":"e_1_2_1_9_1","volume-title":"Proc. IFIP Congress. 65","author":"Dijkstra Edsger W.","year":"1965","unstructured":"Edsger W. Dijkstra. 1965. Programming Considered as a Human Activity. In Proc. IFIP Congress. 65, 213\u2013217. http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd01xx\/EWD117.PDF"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604151"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0243-x"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2210.05420"},{"key":"e_1_2_1_13_1","volume-title":"The Science of Programming","author":"Gries David","unstructured":"David Gries. 1989. The Science of Programming. Springer New York. isbn:978-0-387-96480-5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.46298\/entics.14797"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","unstructured":"Harrison Grodin Runming Li and Robert Harper. 2025. Abstraction Functions as Types (Artifact). Zenodo. https:\/\/doi.org\/10.5281\/zenodo.17344235 10.5281\/zenodo.17344235","DOI":"10.5281\/zenodo.17344235"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632852"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1978.3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96744"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90030-2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00163-6"},{"key":"e_1_2_1_22_1","first-page":"83","article-title":"Semantical Considerations on Modal Logic","volume":"16","author":"Kripke Saul","year":"1963","unstructured":"Saul Kripke. 1963. Semantical Considerations on Modal Logic. Acta Philosophica Fennica, 16 (1963), 83\u201394.","journal-title":"Acta Philosophica Fennica"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0954-6"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Runming Li Harrison Grodin and Robert Harper. 2023. A Verified Cost Analysis of Joinable Red-Black Trees. https:\/\/doi.org\/10.48550\/arXiv.2309.11056 arxiv:2309.11056. 10.48550\/arXiv.2309.11056","DOI":"10.48550\/arXiv.2309.11056"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Runming Li and Robert Harper. 2025. Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability. https:\/\/doi.org\/10.48550\/arXiv.2504.12464 arxiv:2504.12464. 10.48550\/arXiv.2504.12464","DOI":"10.48550\/arXiv.2504.12464"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/942572.807045"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1080\/00927878108822672"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_19"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Tobias Nipkow (Ed.). 2025. Functional Data Structures and Algorithms: A Proof Assistant Approach (1 ed.). 67 Association for Computing Machinery New York NY USA. isbn:979-8-4007-3157-0 https:\/\/doi.org\/10.1145\/3731369 10.1145\/3731369","DOI":"10.1145\/3731369"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498670"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_2_1_33_1","volume-title":"Purely Functional Data Structures","author":"Okasaki Chris","unstructured":"Chris Okasaki. 1999. Purely Functional Data Structures. Cambridge University Press. isbn:978-0-521-66350-2"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.24"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15198-2_7"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:2)2020"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17336-3"},{"key":"e_1_2_1_41_1","unstructured":"Alexander A. Stepanov. 1995. Al Stevens Interviews Alex Stepanov. https:\/\/stepanovpapers.com\/drdobbs-interview.html"},{"key":"e_1_2_1_42_1","volume-title":"First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. Ph. D. Dissertation","author":"Sterling Jonathan","unstructured":"Jonathan Sterling. 2021. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. Ph. D. Dissertation. Carnegie Mellon University."},{"key":"e_1_2_1_43_1","unstructured":"Jonathan Sterling. 2022. Na\u00efve Logical Relations in Synthetic Tait Computability."},{"key":"e_1_2_1_44_1","unstructured":"Jonathan Sterling. 2025. private communication."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.5"},{"key":"e_1_2_1_47_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Univalent Foundations Program."},{"key":"e_1_2_1_48_1","unstructured":"Matthijs V\u00e1k\u00e1r. 2017. In Search of Effectful Dependent Types. University of Oxford. https:\/\/ora.ox.ac.uk\/objects\/uuid:e91e19b3-7e10-4fda-9433-f23b469e4049"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41653"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2631168"},{"key":"e_1_2_1_52_1","volume-title":"Structure and Language of Higher-Order Algebraic Effects. Ph. D. Dissertation","author":"Yang Zhixuan","unstructured":"Zhixuan Yang. 2024. Structure and Language of Higher-Order Algebraic Effects. Ph. D. Dissertation. Imperial College London. https:\/\/yangzhixuan.github.io\/pdf\/yang-thesis.pdf"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776673","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:04:29Z","timestamp":1767899069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776673"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":52,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776673"],"URL":"https:\/\/doi.org\/10.1145\/3776673","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}