{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:58:27Z","timestamp":1787068707040,"version":"3.56.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["206263"],"award-info":[{"award-number":["206263"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003151","name":"Fonds de recherche du Qu\u00e9bec \u2013 Nature et technologies","doi-asserted-by":"publisher","award":["253521"],"award-info":[{"award-number":["253521"]}],"id":[{"id":"10.13039\/501100003151","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003151","name":"Fonds de recherche du Qu\u00e9bec \u2013 Nature et technologies","doi-asserted-by":"publisher","award":["333531"],"award-info":[{"award-number":["333531"]}],"id":[{"id":"10.13039\/501100003151","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":[[2025,8,5]]},"abstract":"<jats:p>Proof assistants based on type theories have been widely successful from verifying safety-critical software to establishing a new standard of rigour by formalizing mathematics. But these proof assistants and even their type-checking kernels are also complex pieces of software, and software invariably has bugs, so why should we trust such proof assistants?<\/jats:p>\n                  <jats:p>\n                    In this paper, we describe the McTT (Mechanized Type Theory) infrastructure to build a verified implementation of a kernel for a core Martin-L\u00f6f type theory (MLTT). McTT is implementation in\n                    <jats:sc>Rocq<\/jats:sc>\n                    and consists of two main components: In the theoretical component, we specify the type theory and prove theorems such as normalization, consistency and injectivity of type constructors of MLTT using an untyped domain model. In the algorithmic component, we relate the declarative specification of typing and the model of normalization in the theoretical component with a functional implementation within\n                    <jats:sc>Rocq<\/jats:sc>\n                    . From this algorithmic component, we extract an OCaml implementation and couple it with a front-end parser for execution. This extracted OCaml code is comparable to what a skilled human programmer would have written and we have successfully used it to type-check a series of small-scale examples.\n                  <\/jats:p>\n                  <jats:p>McTT provides a fully verified kernel for a core MLTT with a full cumulative universe hierarchy. Every step in the compilation pipeline is verified except for the lexer and pretty-printer. As a result, McTT serves both as a framework to explore the meta-theory of advanced type theories and to investigate optimizations of and extensions to the type-checking kernel.<\/jats:p>","DOI":"10.1145\/3747511","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"190-221","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["McTT: A Verified Kernel for a Proof Assistant"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6338-2155","authenticated-orcid":false,"given":"Junyoung","family":"Jang","sequence":"first","affiliation":[{"name":"McGill University, Montreal, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4640-4102","authenticated-orcid":false,"given":"Antoine","family":"Gaulin","sequence":"additional","affiliation":[{"name":"McGill University, Montreal, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6710-6262","authenticated-orcid":false,"given":"Jason Z. S.","family":"Hu","sequence":"additional","affiliation":[{"name":"Amazon, Seattle, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2549-4276","authenticated-orcid":false,"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[{"name":"McGill University, Montreal, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"Andreas Abel. 2013. Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation Thesis. Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen Munich Germany. https:\/\/www.cse.chalmers.se\/~abela\/habil.pdf"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110277"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","unstructured":"Arthur Adjedje Meven Lennon-Bertrand Kenji Maillard Pierre-Marie P\u00e9drot and Lo\u00efc Pujet. 2024. Martin-L\u00f6f \u00e0 la Coq. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP 2024 London UK \ud835\udca5anuary 15\u201316 2024 Amin Timany Dmitriy Traytel Brigitte Pientka and Sandrine Blazy (Eds.). ACM 230\u2013245. doi:10.1145\/3636501.3636951","DOI":"10.1145\/3636501.3636951"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_27"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Thorsten Altenkirch and Ambrus Kaposi. 2016a. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction FSCD 2016 Porto Portugal June 22\u201326 2016 (LIPIcs Vol. 52) Delia Kesner and Brigitte Pientka (Eds.). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik 6:1\u20136:16. doi:10.4230\/LIPIcs.FSCD.2016.6","DOI":"10.4230\/LIPIcs.FSCD.2016.6"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","unstructured":"Thorsten Altenkirch and Ambrus Kaposi. 2016b. Type Theory in Type Theory Using Quotient Inductive Types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2016 St. Petersburg Florida USA January 20\u201322 2016. ACM 18\u201329. doi:10.1145\/2837614.2837638","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:1)2017"},{"key":"e_1_3_2_11_1","unstructured":"Ali Assaf Gilles Dowek Jean-Pierre Jouannaud and Jiaxiang Liu. 2016. Encoding Proofs in Dedukti: the case of Coq proofs. In Proceedings Hammers for Type Theories. 1\u20136. https:\/\/inria.hal.science\/hal-01330980"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2591012"},{"key":"e_1_3_2_13_1","unstructured":"Bruno Barras and Benjamin Werner. 1997. Coq in Coq. https:\/\/www.lix.polytechnique.fr\/Labo\/Bruno.Barras\/public\/coqintro.pdf Unpublished manuscript."},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","unstructured":"Ulrich Berger and Helmut Schwichtenberg. 1991. An Inverse of the Evaluation Functional for Typed Lambda-calculus. In Proceedings of the 6th Annual Symposium on Logic in Computer Science LICS 1991 Amsterdam the Netherlands \ud835\udca5uly 15\u201318 1991 IEEE Computer Society . 203\u2013211. doi:10.1109\/LICS.1991.151645","DOI":"10.1109\/LICS.1991.151645"},{"key":"e_1_3_2_15_1","unstructured":"Mathieu Boespflug and Guillaume Burel. 2012. CoqInE: Translating the Calculus of Inductive Constructions into the \u03bb\u03a0-calculus Modulo. In Workshop on Proof Exchange for Theorem Proving (PxTP) (CEUR Workshop Proceedings Vol. 878) CEUR-WS.org 44\u201350."},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.07.084"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Kevin Buzzard Johan Commelin and Patrick Massot. 2020. Formalising perfectoid spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP 2020 New Orleans LA USA. Association for Computing Machinery 299\u2013312. doi:10.1145\/3372885.3373830","DOI":"10.1145\/3372885.3373830"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"James Chapman. 2008. Type Theory Should Eat Itself. In Proceedings of the International Workshop on Logical Frameworks and Meta\u2013languages: Theory and Practice LFMTP@LICS 2008 Pittsburgh Pennsylvania USA June 23 2008 (Electronic Notes in Theoretical Computer Science Vol. 228) Andreas Abel and Christian Urban (Eds.). Elsevier 21\u201336. doi:10.1016\/J.ENTCS.2008.12.114","DOI":"10.1016\/J.ENTCS.2008.12.114"},{"key":"e_1_3_2_20_1","article-title":"Canonicity and normalisation for Dependent Type Theory.","author":"Coquand Thierry","year":"2018","unstructured":"Thierry Coquand. 2018. Canonicity and normalisation for Dependent Type Theory. CoRR, abs\/1810.09367 (2018). arXiv:http:\/\/arxiv.org\/abs\/1810.09367","journal-title":"CoRR"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129596002150"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Peter Dybjer. 1995. Internal Type Theory. In International Workshop on Types for Proofs and Programs TYPES 1995 Torino Italy June 5\u20138 1995 (Lecture Notes in Computer Science Vol. 1158) Stefano Berardi and Mario Coppo (Eds.). Springer 120\u2013134. doi:10.1007\/3-540-61780-9_66","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00096-9"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796823000060"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Jason Z. S. Hu and Brigitte Pientka. 2022. A Categorical Normalization Proof for the Modal Lambda-Calculus. In Proceedings of the 38th Conference on the Mathematical Foundations of Programming Semantics MFPS 2022 Cornell University Ithaca New York USA with a satellite at IRIF Ennis Diderot University Paris France and online July 11\u201313 2022 (EPTCS Vol. 1) Justin Hsu and Christine Tasson (Eds.). Episciences. doi:10.46298\/ENTICS.103600","DOI":"10.46298\/ENTICS.103600"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Junyoung Jang Antoine Gaulin Jason Z. S. Hu and Brigitte Pientka. 2025. McTT: A Verified Kernel for a Proof Assistant. doi:10.5281\/zenodo.15712175","DOI":"10.5281\/zenodo.15712175"},{"key":"e_1_3_2_30_1","unstructured":"Dominique Larchey-Wendling and Jean-Fran\u00e7ois Monin. 2018. Simulating Induction-Recursion for Partial Algorithms. In 24th International Conference on Types for Proofs and Programs TYPES 2018 Braga Portugal. https:\/\/hal.science\/hal-02333374"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704843"},{"key":"e_1_3_2_34_1","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Studies in proof theory Vol. 1. Bibliopolis."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","unstructured":"Per Martin-L\u00f6f. 1975. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium 1973 H.E. Rose and J.C. Shepherdson (Eds.). Studies in Logic and the Foundations of Mathematics Vol. 80. Elsevier 73\u2013118. doi:10.1016\/S0049-237X(08)71945-1","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","unstructured":"Christine Paulin-Mohring. 1993. Inductive Definitions in the System Coq - Rules and Properties. In Typed Lambda Calculi and Applications International Conference on Typed Lambda Calculi and Applications TLCA\u201993 Utrecht the Netherlands March 16\u201318 1993 (Lecture Notes in Computer Science Vol. 664) Marc Bezem and Jan Friso Groote (Eds.). Springer 328\u2013345. doi:10.1007\/BFb0037116","DOI":"10.1007\/BFb0037116"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571739"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"The Mathlib Community. 2020. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP 2020 New Orleans Louisiana USA January 20\u201321 2020 Jasmin Blanchette and Catalin Hritcu (Eds.). ACM 367\u2013381. doi:10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547649"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","unstructured":"Pawe\u0142 Wieczorek and Dariusz Biernacki. 2018. A Coq Formalization of Normalization by Evaluation for Martin-L\u00f6f Type Theory. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP 2018 Los Angeles California USA \ud835\udca5anuary 8\u20139 2018 June Andronick and Amy P. Felty (Eds.). ACM 266\u2013279. doi:10.1145\/3167091","DOI":"10.1145\/3167091"},{"key":"e_1_3_2_48_1","unstructured":"Th\u00e9o Winterhalter. 2023. Composable partial functions in Coq totally for free. In 29th International Conference on Types for Proofs and Programs TYPES 2023 \u2013 Abstracts 208."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747511","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T09:59:41Z","timestamp":1784195981000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747511"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":47,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747511"],"URL":"https:\/\/doi.org\/10.1145\/3747511","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}