{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T18:10:32Z","timestamp":1775671832431,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":100,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Foundation","award":["2211996"],"award-info":[{"award-number":["2211996"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2442461"],"award-info":[{"award-number":["2442461"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"United States Air Force Office of Scientific Research","award":["FA9550-21-0009"],"award-info":[{"award-number":["FA9550-21-0009"]}]},{"name":"United States Air Force Office of Scientific Research","award":["FA9550-23-1-0434"],"award-info":[{"award-number":["FA9550-23-1-0434"]}]},{"name":"United States Air Force Office of Scientific Research","award":["FA9550-21-1-0385"],"award-info":[{"award-number":["FA9550-21-1-0385"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779085","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"231-247","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Mechanizing Synthetic Tait Computability in Istari"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7600-9069","authenticated-orcid":false,"given":"Runming","family":"Li","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8523-5156","authenticated-orcid":false,"given":"Yue","family":"Yao","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9400-2941","authenticated-orcid":false,"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"The 1Lab Development Team. 2024. The 1Lab Normalisation by evaluation. https:\/\/1lab.dev\/Cat.CartesianClosed.Free.html##normalisation-by-evaluation"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_3_2_1_5_1","unstructured":"Emmanuel Su\u00e1rez Acevedo and Stephanie Weirich. 2023. Making Logical Relations More Relatable (Proof Pearl). arxiv:2309.15724. arxiv:2309.15724"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636951"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632920"},{"key":"e_1_3_2_1_9_1","unstructured":"Thorsten Altenkirch Martin Hofmann and Thomas Streicher. 1996. Reduction-free Normalisation for System F. Available at https:\/\/people.cs.nott.ac.uk\/psztxa\/publ\/f97.pdf"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_1_11_1","volume-title":"Computational Semantics of Cartesian Cubical Type Theory. Ph. D. Dissertation","author":"Angiuli Carlo","unstructured":"Carlo Angiuli. 2019. Computational Semantics of Cartesian Cubical Type Theory. Ph. D. Dissertation. Carnegie Mellon University. https:\/\/carloangiuli.com\/papers\/thesis.pdf"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000347"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.274.1"},{"key":"e_1_3_2_1_14_1","unstructured":"Carlo Angiuli and Daniel Gratzer. 2025. Principles of Dependent Type Theory. https:\/\/carloangiuli.com\/papers\/type-theory-book.pdf"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2018.6"},{"key":"e_1_3_2_1_16_1","volume-title":"Category Theory","author":"Awodey Steve","year":"1992","unstructured":"Steve Awodey. 2010. Category Theory (2nd ed.). Oxford University Press, Inc., USA. isbn:0199237182","edition":"2"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2016.5"},{"key":"e_1_3_2_1_19_1","volume-title":"Fiore","author":"Berry David G.","year":"2025","unstructured":"David G. Berry and Marcelo P. Fiore. 2025. Formal P-Category Theory and Normalization by Evaluation in Rocq. arxiv:2505.07780. arxiv:2505.07780"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.23"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2023.18"},{"key":"e_1_3_2_1_22_1","unstructured":"N. Bourbaki M. Artin A. Grothendieck P. Deligne and J.L. Verdier. 1983. Theorie des Topos et Cohomologie Etale des Schemas. Seminaire de Geometrie Algebrique du Bois-Marie 1963-1964 (SGA 4): Tome 1. Springer Berlin Heidelberg. isbn:978-3-540-05896-0"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000154"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2019.2"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_3_2_1_26_1","volume-title":"Smith","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable, Stuart F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, NJ."},{"key":"e_1_3_2_1_27_1","unstructured":"Thierry Coquand. 2018. Canonicity and normalisation for Dependent Type Theory. arxiv:1810.09367. arxiv:1810.09367"},{"key":"e_1_3_2_1_28_1","unstructured":"Karl Crary. 2025. Istari. GitHub. https:\/\/github.com\/kcrary\/istari"},{"key":"e_1_3_2_1_29_1","unstructured":"Karl Crary. 2025. The Istari Proof Assistant. https:\/\/istarilogic.org\/ Accessed: 2025-09-08"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172707"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3776645"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1215\/ijm\/1256068141"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_3_2_1_35_1","volume-title":"11th International Workshop on Coq for Programming Languages (CoqPL), https:\/\/www.cs.cmu.edu\/~balzers\/publications\/coqpl-2025","author":"Gollamudi Tarakaram","year":"2025","unstructured":"Tarakaram Gollamudi, Jules Jacobs, Yue Yao, and Stephanie Balzer. 2025. A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types. 11th International Workshop on Coq for Programming Languages (CoqPL), https:\/\/www.cs.cmu.edu\/~balzers\/publications\/coqpl-2025.pdf"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532398"},{"key":"e_1_3_2_1_37_1","unstructured":"Daniel Gratzer Michael Shulman and Jonathan Sterling. 2024. Strict universes for Grothendieck topoi. arxiv:2202.12012"},{"key":"e_1_3_2_1_38_1","unstructured":"Daniel Gratzer and Jonathan Sterling. 2021. Syntactic categories for dependent type theory: sketching and adequacy. arxiv:2012.10783. arxiv:2012.10783"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2210.05420"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Daniel R. Grayson Benedikt Ahrens Ralph Matthes Niels van der Weide Anders M\u00f6rtberg cathlelay Langston Barrett Peter LeFanu Lumsdaine Marco Maggesi Vladimir Voevodsky Tomi Pannila Gianluca Amato Michael Lindgren Mitchell Riley Skantz CalosciMatteo Arnoud van der Leer Tobias-Schmude Daniel Frumin Auke Booij Hichem Saghrouni Dennis varkor Dimitris Tsementzis niccoloveltri Anthony Bordg Dominik Kirst Karl Palmskog Satoshi Kura and Tamara von Glehn. 2025. UniMath\/UniMath: v20250923. https:\/\/doi.org\/10.5281\/zenodo.17186647 Version v20250923 10.5281\/zenodo.17186647","DOI":"10.5281\/zenodo.17186647"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.46298\/entics.14797"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3776673"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632852"},{"key":"e_1_3_2_1_45_1","unstructured":"Robert Harper. 2021. An Equational Logical Framework for Type Theories. arxiv:2106.01484"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96744"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Jason Hickey Aleksey Nogin Robert Constable Brian Aydemir Yegor Bryukhov Richard Eaton Adam Granicz Christoph Kreitz Vladimir Krupski Lori Lorigo Carl Witty and Xin Yu. 2003. MetaPRL - A Modular Logical Environment. 10.","DOI":"10.1007\/10930755_19"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39174"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439922"},{"key":"e_1_3_2_1_51_1","unstructured":"Xu Huang. 2023. Synthetic Tait Computability the Hard Way. arxiv:2310.02051. arxiv:2310.02051"},{"key":"e_1_3_2_1_52_1","volume-title":"Sketches of an Elephant: A Topos Theory Compendium","author":"Johnstone Peter T.","year":"1985","unstructured":"Peter T. Johnstone. 2002. Sketches of an Elephant: A Topos Theory Compendium, Volume 1. Clarendon Press, Oxford. isbn:9780198534259"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.25"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3747535"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2024.10"},{"key":"e_1_3_2_1_57_1","volume-title":"Amortized Analysis of Splay Trees via a Lax Homomorphism","author":"Kebuladze Lukas","unstructured":"Lukas Kebuladze. 2025. Amortized Analysis of Splay Trees via a Lax Homomorphism. Carnegie Mellon University. https:\/\/www.cs.cmu.edu\/~runmingl\/student\/kebuladze-splay.pdf"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3776685"},{"key":"e_1_3_2_1_59_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_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.50.5.869"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0954-6"},{"key":"e_1_3_2_1_62_1","unstructured":"Runming Li Harrison Grodin and Robert Harper. 2023. A Verified Cost Analysis of Joinable Red-Black Trees. arxiv:2309.11056. arxiv:2309.11056"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","unstructured":"Runming Li and Robert Harper. 2025. Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability. April https:\/\/doi.org\/10.48550\/arXiv.2504.12464 arXiv:2504.12464 [cs] 10.48550\/arXiv.2504.12464","DOI":"10.48550\/arXiv.2504.12464"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","unstructured":"Runming Li Yue Yao and Robert Harper. 2025. Mechanizing Synthetic Tait Computability in Istari (Artifact). https:\/\/doi.org\/10.5281\/zenodo.17808361 10.5281\/zenodo.17808361","DOI":"10.5281\/zenodo.17808361"},{"key":"e_1_3_2_1_65_1","volume-title":"Functional Pearl: Short and Mechanized Logical Relation for Dependent Type Theories. https:\/\/electriclam.com\/papers\/mltt.pdf","author":"Liu Yiyun","year":"2025","unstructured":"Yiyun Liu, Jonathan Chan, and Stephanie Weirich. 2025. Functional Pearl: Short and Mechanized Logical Relation for Dependent Type Theories. https:\/\/electriclam.com\/papers\/mltt.pdf"},{"key":"e_1_3_2_1_66_1","volume-title":"Intuitionistic Type Theory. https:\/\/archive-pml.github.io\/martin-lof\/pdfs\/Bibliopolis-Book-retypeset-1984.pdf Lecture notes Padua","author":"Martin-L\u00f6f Per","year":"1984","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. https:\/\/archive-pml.github.io\/martin-lof\/pdfs\/Bibliopolis-Book-retypeset-1984.pdf Lecture notes Padua 1984, Bibliopolis, Napoli"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_69_1","volume-title":"Logic for Computable Functions: description of a machine implementation","author":"Milner Robin","unstructured":"Robin Milner. 1972. Logic for Computable Functions: description of a machine implementation.. Stanford, CA, USA."},{"key":"e_1_3_2_1_70_1","volume-title":"Mitchell and Andre Scedrov","author":"John","year":"1992","unstructured":"John C. Mitchell and Andre Scedrov. 1992. Notes on Sconing and Relators. In Selected Papers from the Workshop on Computer Science Logic (CSL \u201992). Springer-Verlag, Berlin, Heidelberg. 352\u2013378. isbn:3540569928"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498670"},{"key":"e_1_3_2_1_72_1","volume-title":"Smith","author":"Nordstr\u00f6m Bengt","year":"1990","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-L\u00f6f\u2019s type theory: an introduction. Clarendon Press, USA. isbn:0198538146"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.24"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394740"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_3_2_1_76_1","volume-title":"Category Theory in Context","author":"Riehl Emily","unstructured":"Emily Riehl. 2016. Category Theory in Context. Dover Publications. isbn:978-0-486-80903-8"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:2)2020"},{"key":"e_1_3_2_1_79_1","volume-title":"Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Interactive Theorem Proving - 6th International Conference, ITP","author":"Sch\u00e4fer Steven","year":"2015","unstructured":"Steven Sch\u00e4fer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Xingyuan Zhang and Christian Urban (Eds.) (LNAI). Springer-Verlag."},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294101"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6990769"},{"key":"e_1_3_2_1_83_1","unstructured":"Jonathan Sterling. 2022. Na\u00efve Logical Relations in Synthetic Tait Computability. https:\/\/www.jonmsterling.com\/bafkrmialyvkzh6w6snnzr3k4h2b62bztsk4le57idughqik24bltinieki.pdf"},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.31"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(1:43)2022"},{"key":"e_1_3_2_1_87_1","unstructured":"Jonathan Sterling Daniel Gratzer and Lars Birkedal. 2023. Denotational semantics of general store and polymorphism. arxiv:2210.02169. arxiv:2210.02169"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.5"},{"key":"e_1_3_2_1_90_1","unstructured":"Jonathan Sterling and Bas Spitters. 2018. Normalization by gluing for free \u03bb -theories. arxiv:1809.08646"},{"key":"e_1_3_2_1_91_1","volume-title":"Intensional Interpretations of Functionals of Finite Type I. 32, 2","author":"Tait W. W.","year":"1967","unstructured":"W. W. Tait. 1967. Intensional Interpretations of Functionals of Finite Type I. 32, 2 (1967), 198\u2013212. issn:00224812 http:\/\/www.jstor.org\/stable\/2271658"},{"key":"e_1_3_2_1_92_1","unstructured":"The RedPRL Development Team. 2018. redtt. https:\/\/www.github.com\/RedPRL\/redtt"},{"key":"e_1_3_2_1_93_1","unstructured":"Taichi Uemura. 2021. Abstract and Concrete Type Theories. Ph. D. Dissertation. Universiteit van Amsterdam. https:\/\/www.illc.uva.nl\/cms\/Research\/Publications\/Dissertations\/DS-2021-09.text.pdf"},{"key":"e_1_3_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167091"},{"key":"e_1_3_2_1_95_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"},{"key":"e_1_3_2_1_96_1","unstructured":"Zhixuan Yang. 2025. Revisiting the Logical Framework for Locally Cartesian Closed Categories. https:\/\/yangzhixuan.github.io\/pdf\/lcclf.pdf"},{"key":"e_1_3_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2511.05739"},{"key":"e_1_3_2_1_98_1","unstructured":"Tesla Zhang. 2024. Three non-cubical applications of extension types. arxiv:2311.05658. arxiv:2311.05658"},{"key":"e_1_3_2_1_99_1","unstructured":"Tesla Zhang Sonya Simkin Rui Li Yue Yao and Stephanie Balzer. 2025. A Language-Agnostic Logical Relation for Message-Passing Protocols. arxiv:2506.10026. arxiv:2506.10026"},{"key":"e_1_3_2_1_100_1","volume-title":"Formally Verified Cost of the Parallel Prefix Sum Algorithm","author":"Zhou Andrew","unstructured":"Andrew Zhou. 2025. Formally Verified Cost of the Parallel Prefix Sum Algorithm. Carnegie Mellon University. https:\/\/www.cs.cmu.edu\/~runmingl\/student\/zhou-scan.pdf"}],"event":{"name":"CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Rennes France","acronym":"CPP '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779085","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779085","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:53:41Z","timestamp":1775667221000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779085"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":100,"alternative-id":["10.1145\/3779031.3779085","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779085","relation":{},"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}