{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T18:10:45Z","timestamp":1775671845338,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":71,"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":"Air Force Office of Scientific Research","award":["FA9550-21-1-0009"],"award-info":[{"award-number":["FA9550-21-1-0009"]}]},{"name":"National Science Foundation","award":["2434614"],"award-info":[{"award-number":["2434614"]}]},{"name":"European Union","award":["ERC, Nekoka, 101083038"],"award-info":[{"award-number":["ERC, Nekoka, 101083038"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779087","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"88-103","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Certifying Proof Assistant for Synthetic Mathematics in Lean"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8839-0618","authenticated-orcid":false,"given":"Wojciech","family":"Nawrocki","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-7993-3517","authenticated-orcid":false,"given":"Joseph","family":"Hua","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0470-5249","authenticated-orcid":false,"given":"Mario","family":"Carneiro","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-4006-0983","authenticated-orcid":false,"given":"Yiming","family":"Xu","sequence":"additional","affiliation":[{"name":"LMU Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-0943-7560","authenticated-orcid":false,"given":"Spencer","family":"Woolfson","sequence":"additional","affiliation":[{"name":"Chapman University, Orange, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-6492-5428","authenticated-orcid":false,"given":"Shuge","family":"Rong","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7921-9149","authenticated-orcid":false,"given":"Sina","family":"Hazratpour","sequence":"additional","affiliation":[{"name":"Stockholm University, Stockholm, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-179X","authenticated-orcid":false,"given":"Steve","family":"Awodey","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","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_2"},{"key":"e_1_3_2_1_3_1","unstructured":"Andreas Abel. 2013. Normalization by evaluation: Dependent types and impredicativity. Ph. D. Dissertation. Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_3_2_1_5_1","volume-title":"Spivak","author":"Aberl\u00e9 C. B.","year":"2025","unstructured":"C. B. Aberl\u00e9 and David I. Spivak. 2025. Polynomial Universes in Homotopy Type Theory. arxiv:2409.19176. arxiv:2409.19176"},{"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.4230\/LIPIcs.CSL.2017.8"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000312"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_1_10_1","unstructured":"Carlo Angiuli and Daniel Gratzer. 2024. Principles of Dependent Type Theory. https:\/\/www.danielgratzer.com\/papers\/type-theory-book.pdf"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"e_1_3_2_1_12_1","unstructured":"Steve Awodey. 2025. Algebraic Type Theory Part 1: Martin-L\u00f6f algebras. arXiv preprint arXiv:2505.10761v1."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.049"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"e_1_3_2_1_15_1","first-page":"39","volume-title":"TYPES 2017","author":"Bauer Andrej","year":"2017","unstructured":"Andrej Bauer, Philipp Haselwarter, and Th\u00e9o Winterhalter. 2017. A modular formalization of type theory in Coq. TYPES 2017, https:\/\/types2017.elte.hu\/proc.pdf##page=39"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2013.107"},{"key":"e_1_3_2_1_17_1","unstructured":"Mark Bickford. 2020. Cubical type theory with several universes in Nuprl. https:\/\/hott-uf.github.io\/2020\/HoTTUF_2020_paper_12.pdf"},{"key":"e_1_3_2_1_18_1","unstructured":"Ingo Blechschmidt. 2021. Using the internal language of toposes in algebraic geometry. arXiv preprint arXiv:2111.03685."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_3_2_1_21_1","volume-title":"Homotopy Type Theory in Lean. CoRR, abs\/1704.06781","author":"Buchholtz Ulrik","year":"2017","unstructured":"Ulrik Buchholtz, Floris van Doorn, and Jakob von Raumer. 2017. Homotopy Type Theory in Lean. CoRR, abs\/1704.06781 (2017), arXiv:1704.06781. arxiv:1704.06781"},{"key":"e_1_3_2_1_22_1","unstructured":"Mario Carneiro. 2025. Lean4Lean: Verifying a Typechecker for Lean in Lean. arxiv:2403.14064. arxiv:2403.14064"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TLCA.2015.138"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2024.3"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_28_1","unstructured":"Thierry Coquand. 2013. Presheaf model of type theory."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90230-Y"},{"key":"e_1_3_2_1_30_1","volume-title":"A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory","author":"de Boer Menno","unstructured":"Menno de Boer. 2020. A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory. Stockholm University, Department of Mathematics."},{"key":"e_1_3_2_1_31_1","unstructured":"Kunhong Du. 2025. On the Formalization of the Simplicial Model of HoTT. Master\u2019s thesis. Rheinischen Friedrich-Wilhelms-Universit\u00e4t Bonn."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"e_1_3_2_1_34_1","unstructured":"Gabriel Ebner. 2022. quote4: Intuitive type-safe expression quotations for Lean 4. https:\/\/github.com\/leanprover-community\/quote4"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110271"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/368892.368907"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004112000394"},{"key":"e_1_3_2_1_38_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 10.5281\/zenodo.17186647","DOI":"10.5281\/zenodo.17186647"},{"key":"e_1_3_2_1_39_1","volume-title":"Poly: A Lean4 Formalization of Polynomial Functors. https:\/\/github.com\/sinhp\/poly","author":"Hazratpour Sina","year":"2024","unstructured":"Sina Hazratpour. 2024. Poly: A Lean4 Formalization of Polynomial Functors. https:\/\/github.com\/sinhp\/poly"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022273"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"e_1_3_2_1_42_1","volume-title":"HoTTLean: Formalizing the Meta-Theory of HoTT in Lean. TYPES","author":"Hua Joseph","year":"2025","unstructured":"Joseph Hua, Steve Awodey, Mario Carneiro, Sina Hazratpour, Wojciech Nawrocki, Spencer Woolfson, and Yiming Xu. 2025. HoTTLean: Formalizing the Meta-Theory of HoTT in Lean. TYPES 2025."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084217"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)X8028-6"},{"key":"e_1_3_2_1_45_1","unstructured":"Andr\u00e9 Joyal. 2017. Notes on clans and tribes. arXiv preprint arXiv:1710.10238."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3747535"},{"key":"e_1_3_2_1_47_1","unstructured":"Chris Kapulkin and Peter LeFanu Lumsdaine. 2018. The Simplicial Model of Univalent Foundations (after Voevodsky). arxiv:1211.2851. arxiv:1211.2851"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511550812"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2022.28"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2025.27"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603153"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-97-8943-6_4"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00012-9"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","unstructured":"Wojciech Nawrocki Joseph Hua Mario Carneiro Yiming Xu Spencer Woolfson Shuge Rong Sina Hazratpour and Steve Awodey. 2025. Implementation of \"A Certifying Proof Assistant for Synthetic Mathematics in Lean\". https:\/\/doi.org\/10.5281\/zenodo.17798253 10.5281\/zenodo.17798253","DOI":"10.5281\/zenodo.17798253"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277752"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63334-3_14"},{"key":"e_1_3_2_1_59_1","unstructured":"Egbert Rijke Elisabeth Stenholm Jonathan Prieto-Cubides Fredrik Bakke Vojt\u011bch \u0160t\u011bpan\u010d\u00edk and others. 2025. The Agda-Unimath library. https:\/\/github.com\/UniMath\/agda-unimath\/"},{"key":"e_1_3_2_1_60_1","volume-title":"Ground Zero: Lean 4 HoTT Library. https:\/\/github.com\/rzrn\/ground_zero","year":"2025","unstructured":"rzrn. 2025. Ground Zero: Lean 4 HoTT Library. https:\/\/github.com\/rzrn\/ground_zero"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3706056"},{"key":"e_1_3_2_1_63_1","volume-title":"Types for Proofs and Programs 20th Meeting (TYPES","author":"Sozeau Matthieu","year":"2014","unstructured":"Matthieu Sozeau and Nicolas Tabareau. 2014. Towards an internalization of the groupoid model of type theory. Types for Proofs and Programs 20th Meeting (TYPES 2014), Book of Abstracts."},{"key":"e_1_3_2_1_64_1","volume-title":"First Steps in Synthetic Tait Computability. Ph. D. Dissertation","author":"Sterling Jonathan","unstructured":"Jonathan Sterling. 2021. First Steps in Synthetic Tait Computability. Ph. D. Dissertation. Carnegie Mellon University."},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103723"},{"key":"e_1_3_2_1_67_1","unstructured":"The Agda Community. 2025. Cubical Agda Library. https:\/\/github.com\/agda\/cubical"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000208"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(2:1)2022"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167091"},{"key":"e_1_3_2_1_71_1","volume-title":"31st International Conference on Types for Proofs and Programs.","author":"Xu Yiming","year":"2025","unstructured":"Yiming Xu and Kenji Maillard. 2025. Geometric Reasoning in Lean: from Algebraic Structures to Presheaves. In 31st International Conference on Types for Proofs and Programs."}],"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.3779087","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779087","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:53:50Z","timestamp":1775667230000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779087"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":71,"alternative-id":["10.1145\/3779031.3779087","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779087","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"}}]}}