{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:04Z","timestamp":1780994704900,"version":"3.54.1"},"reference-count":81,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2025,1,27]],"date-time":"2025-01-27T00:00:00Z","timestamp":1737936000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Marie Sk\u00edodowska-Curie","award":["101024493"],"award-info":[{"award-number":["101024493"]}]},{"name":"European Union\u2019s Horizon 2020 Framework Programme","award":["101002277"],"award-info":[{"award-number":["101002277"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2025,2,28]]},"abstract":"<jats:p>\n            <jats:sc>Coq<\/jats:sc>\n            is built around a well-delimited kernel that performs type checking for definitions in a variant of the Calculus of Inductive Constructions (\n            <jats:sc>CIC<\/jats:sc>\n            ). Although the metatheory of\n            <jats:sc>CIC<\/jats:sc>\n            is very stable and reliable, the correctness of its implementation in\n            <jats:sc>Coq<\/jats:sc>\n            is less clear. Indeed, implementing an efficient type checker for\n            <jats:sc>CIC<\/jats:sc>\n            is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in\n            <jats:sc>Coq<\/jats:sc>\n            . This article presents the first implementation of a type checker for the kernel of\n            <jats:sc>Coq<\/jats:sc>\n            (without the module system, template polymorphism and \u03b7-conversion), which is proven sound and complete in\n            <jats:sc>Coq<\/jats:sc>\n            with respect to its formal specification. Note that because of G\u00f6del\u2019s second incompleteness theorem, there is no hope to prove completely the soundness of the specification of\n            <jats:sc>Coq<\/jats:sc>\n            inside\n            <jats:sc>Coq<\/jats:sc>\n            (in particular strong normalization), but it is possible to prove the correctness and completeness of the implementation assuming soundness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the\n            <jats:sc>MetaCoq<\/jats:sc>\n            project which provides meta-programming facilities to work with terms and declarations at the level of the kernel. We verify a relatively efficient type checker based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (\n            <jats:sc>PCUIC<\/jats:sc>\n            ) at the basis of\n            <jats:sc>Coq<\/jats:sc>\n            . It is worth mentioning that during the verification process, we have found a source of incompleteness in\n            <jats:sc>Coq<\/jats:sc>\n            \u2019s official type checker, which has then been fixed in\n            <jats:sc>Coq<\/jats:sc>\n            8.14 thanks to our work. In addition to the kernel implementation, another essential feature of\n            <jats:sc>Coq<\/jats:sc>\n            is the so-called\n            <jats:italic>extraction<\/jats:italic>\n            mechanism: the production of executable code in functional languages from\n            <jats:sc>Coq<\/jats:sc>\n            definitions. We present a verified version of this subtle type and proof erasure step, therefore enabling the verified extraction of a safe type checker for\n            <jats:sc>Coq<\/jats:sc>\n            in the future.\n          <\/jats:p>","DOI":"10.1145\/3706056","type":"journal-article","created":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T09:52:26Z","timestamp":1732701146000},"page":"1-74","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Correct and Complete Type Checking and Certified Erasure for\n            <scp>Coq<\/scp>\n            , in\n            <scp>Coq<\/scp>"],"prefix":"10.1145","volume":"72","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6452-8806","authenticated-orcid":false,"given":"Matthieu","family":"Sozeau","sequence":"first","affiliation":[{"name":"Inria, Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8676-9819","authenticated-orcid":false,"given":"Yannick","family":"Forster","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7079-8826","authenticated-orcid":false,"given":"Meven","family":"Lennon-Bertrand","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0459-2678","authenticated-orcid":false,"given":"Jakob","family":"Nielsen","sequence":"additional","affiliation":[{"name":"Concordium Blockchain Research Center, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9881-3696","authenticated-orcid":false,"given":"Th\u00e9o","family":"Winterhalter","sequence":"additional","affiliation":[{"name":"Inria Research Centre Saclay \u00cele-de-France, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,27]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_3_3_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_8"},{"key":"e_1_3_3_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_3_3_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"e_1_3_3_6_1","volume-title":"Proceedings of the 13th International Conference on Interactive Theorem Proving","author":"Abrahamsson Oskar","year":"2022","unstructured":"Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. 2022. Candle: A verified implementation of HOL light. In Proceedings of the 13th International Conference on Interactive Theorem Proving. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik."},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636951"},{"key":"e_1_3_3_8_1","volume-title":"Proceedings of the The 3rd International Workshop on Coq for Programming Languages","author":"Anand Abhishek","year":"2017","unstructured":"Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for coq. In Proceedings of the The 3rd International Workshop on Coq for Programming Languages. Paris, France. Retrieved from http:\/\/conf.researchr.org\/event\/CoqPL-2017\/main-certicoq-a-verified-compiler-for-coq"},{"key":"e_1_3_3_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_2"},{"key":"e_1_3_3_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_3"},{"key":"e_1_3_3_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439934"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796822000077"},{"key":"e_1_3_3_13_1","volume-title":"Requirements on the Use of Coq in the Context of Common Criteria Evaluations","year":"2021","unstructured":"ANSSI. 2021. Requirements on the Use of Coq in the Context of Common Criteria Evaluations. v1.1. French National Cybersecurity Agency. Retrieved from https:\/\/www.ssi.gouv.fr\/uploads\/2014\/11\/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.1-en.pdf"},{"key":"e_1_3_3_14_1","volume-title":"Coq en Coq","author":"Barras Bruno","year":"1996","unstructured":"Bruno Barras. 1996. Coq en Coq. Rapport de Recherche 3026. INRIA."},{"key":"e_1_3_3_15_1","volume-title":"Auto-validation D\u2019un Syst\u00e8me de Preuves Avec Familles Inductives","author":"Barras Bruno","year":"1999","unstructured":"Bruno Barras. 1999. Auto-validation D\u2019un Syst\u00e8me de Preuves Avec Familles Inductives. Th\u00e8se de Doctorat. Universit\u00e9 Paris 7. Retrieved from http:\/\/pauillac.inria.fr\/barras\/publi\/these_barras.ps.gz"},{"key":"e_1_3_3_16_1","volume-title":"Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families","author":"Barras Bruno","year":"2012","unstructured":"Bruno Barras. 2012. Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families. Habilitation Thesis."},{"key":"e_1_3_3_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2756553"},{"key":"e_1_3_3_19_1","volume-title":"Un Calcul des Constructions Implicite Avec Sommes D\u00e9pendantes et \u00e0 Inf\u00e9rence de Type d\u00e9cidable. (An implicit Calculus of Constructions with Dependent Sums and Decidable Type Inference)","author":"Bernardo Bruno","year":"2015","unstructured":"Bruno Bernardo. 2015. Un Calcul des Constructions Implicite Avec Sommes D\u00e9pendantes et \u00e0 Inf\u00e9rence de Type d\u00e9cidable. (An implicit Calculus of Constructions with Dependent Sums and Decidable Type Inference). Ph. D. Dissertation. \u00c9cole Polytechnique, Palaiseau, France. Retrieved from https:\/\/tel.archives-ouvertes.fr\/tel-01197380"},{"key":"e_1_3_3_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2022.01.017"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","unstructured":"Mario Carneiro. 2024. Lean4Lean: Towards a formalized metatheory for the lean theorem prover. (March2024). DOI:10.48550\/ARXIV.2403.14064arxiv:2403.14064 [cs.PL]","DOI":"10.48550\/ARXIV.2403.14064"},{"key":"e_1_3_3_22_1","unstructured":"Jesper Cockx. [n. d.]. Agda Core: The Dream and the Reality. ([n. d.]). Retrieved from https:\/\/jesper.cx\/files\/IFIP28-2024.html"},{"key":"e_1_3_3_23_1","volume-title":"Metamathematical Investigations of a Calculus of Constructions","author":"Coquand T.","year":"1989","unstructured":"T. Coquand. 1989. Metamathematical Investigations of a Calculus of Constructions. Ph. D. Dissertation. Retrieved from https:\/\/hal.inria.fr\/inria-00075471"},{"key":"e_1_3_3_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_3_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"e_1_3_3_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_3_3_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00096-9"},{"key":"e_1_3_3_28_1","volume-title":"Proceedings of the 10th International Conference on Interactive Theorem Proving","author":"Forster Yannick","year":"2019","unstructured":"Yannick Forster and Fabian Kunze. 2019. A certifying extraction with time bounds from coq to call-by-value \u03bb-calculus. In Proceedings of the 10th International Conference on Interactive Theorem Proving. Springer."},{"key":"e_1_3_3_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656379"},{"key":"e_1_3_3_30_1","article-title":"Inconsistency of classical logic in type theory","author":"Geuvers Herman","year":"2007","unstructured":"Herman Geuvers. 2007. Inconsistency of classical logic in type theory. Unpublished Notes (2007). Retrieved from http:\/\/www.cs.ru.nl\/herman\/PUBS\/newnote.ps.gz","journal-title":"Unpublished Notes"},{"key":"e_1_3_3_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/329031610.1145\/3290316"},{"key":"e_1_3_3_32_1","volume-title":"Proceedings of the 29th International Conference on Types for Proofs and Programs","author":"Gilbert Ga\u00ebtan","year":"2023","unstructured":"Ga\u00ebtan Gilbert, Pierre-Marie P\u00e9drot, Matthieu Sozeau, and Nicolas Tabareau. 2023. From lost to the river: Embracing sort proliferation. In Proceedings of the 29th International Conference on Types for Proofs and Programs."},{"key":"e_1_3_3_33_1","volume-title":"Un Calcul de Constructions Infinies et Son Application \u00e0 la v\u00e9rification de Syst\u00e8mes Communicants","author":"Gim\u00e9nez Carlos Eduardo","year":"1996","unstructured":"Carlos Eduardo Gim\u00e9nez. 1996. Un Calcul de Constructions Infinies et Son Application \u00e0 la v\u00e9rification de Syst\u00e8mes Communicants. Ph. D. Dissertation. Ecole Normale Sup\u00e9rieure de Lyon. Retrieved from ftp:\/\/ftp.inria.fr\/INRIA\/LogiCal\/Eduardo.Gimenez\/thesis.ps.gz"},{"key":"e_1_3_3_34_1","volume-title":"Interpr\u00e9tation Fonctionnelle Et \u00e9limination Des Coupures de l\u2019arithm\u00e9tique d\u2019ordre Sup\u00e9rieur","author":"Girard J.-Y.","year":"1972","unstructured":"J.-Y. Girard. 1972. Interpr\u00e9tation Fonctionnelle Et \u00e9limination Des Coupures de l\u2019arithm\u00e9tique d\u2019ordre Sup\u00e9rieur. Ph. D. Dissertation. Universit\u00e9 Paris 7."},{"key":"e_1_3_3_35_1","volume-title":"Vers une Certification de l\u2019extraction de Coq","author":"Glondu St\u00e9phane","year":"2012","unstructured":"St\u00e9phane Glondu. 2012. Vers une Certification de l\u2019extraction de Coq. Ph. D. Dissertation. Universit\u00e9 Paris Diderot."},{"key":"e_1_3_3_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"e_1_3_3_37_1","volume-title":"Proceedings of the 10th Conference on Interactive Theorem Proving","author":"Gu\u00e9neau Arma\u00ebl","year":"2019","unstructured":"Arma\u00ebl Gu\u00e9neau, Jacques-Henri Jourdan, Arthur Chargu\u00e9raud, and Fran\u00e7ois Pottier. 2019. Formal proof and analysis of an incremental cycle detection algorithm. In Proceedings of the 10th Conference on Interactive Theorem Proving. Portland, United States. Retrieved from https:\/\/hal.inria.fr\/hal-02167236"},{"key":"e_1_3_3_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"e_1_3_3_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90108-T"},{"key":"e_1_3_3_40_1","unstructured":"G\u00e9rard Huet. 1988. Extending the Calculus of Constructions with Type:Type. (1988). Retrieved from http:\/\/pauillac.inria.fr\/huet\/PUBLIC\/typtyp.pdf"},{"key":"e_1_3_3_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"e_1_3_3_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014058"},{"issue":"4","key":"e_1_3_3_43_1","article-title":"Proof-irrelevant model of CC with predicative induction and judgmental equality","volume":"7","author":"Lee Gyesik","year":"2011","unstructured":"Gyesik Lee and Benjamin Werner. 2011. Proof-irrelevant model of CC with predicative induction and judgmental equality. Logical Methods in Computer Science 7, 4 (2011).","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_3_44_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.24"},{"key":"e_1_3_3_45_1","volume-title":"Bidirectional Typing for the Calculus of Inductive Constructions","author":"Lennon-Bertrand Meven","year":"2022","unstructured":"Meven Lennon-Bertrand. 2022. Bidirectional Typing for the Calculus of Inductive Constructions. PhD Thesis."},{"key":"e_1_3_3_46_1","first-page":"17","volume-title":"Formalisation et Impl\u00e9mentation Des Propositions Strictes Dans MetaCoq","author":"Leray Yann","year":"2022","unstructured":"Yann Leray. 2022. Formalisation et Impl\u00e9mentation Des Propositions Strictes Dans MetaCoq. Technical Report. Inria Rennes - Bretagne Atlantique ; LS2N-Nantes Universit\u00e9. 17 pages. Retrieved from https:\/\/inria.hal.science\/hal-04433492"},{"key":"e_1_3_3_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_3_48_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Proceedings of the International Workshop on Types for Proofs and Programs.","volume":"2646","author":"Letouzey Pierre","year":"2002","unstructured":"Pierre Letouzey. 2002. A new extraction for coq. In Proceedings of the International Workshop on Types for Proofs and Programs.Herman Geuvers and Freek Wiedijk (Eds.), Lecture Notes in Computer Science, Vol. 2646, Springer, 200\u2013219."},{"key":"e_1_3_3_49_1","volume-title":"Programmation Fonctionnelle Certifi\u00e9e: L\u2019extraction de Programmes Dans l\u2019assistant Coq","author":"Letouzey Pierre","year":"2004","unstructured":"Pierre Letouzey. 2004. Programmation Fonctionnelle Certifi\u00e9e: L\u2019extraction de Programmes Dans l\u2019assistant Coq. Th\u00e8se de Doctorat. Universit\u00e9 Paris-Sud. Retrieved from http:\/\/www.pps.jussieu.fr\/letouzey\/download\/these_letouzey.pdf"},{"key":"e_1_3_3_50_1","series-title":"Studies in Proof Theory","volume-title":"Intuitionistic Type Theory","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."},{"key":"e_1_3_3_51_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.003.0010"},{"key":"e_1_3_3_52_1","unstructured":"Conor McBride. 2009. Grins from my Ripley Cupboard. (2009)."},{"key":"e_1_3_3_53_1","unstructured":"Conor McBride. 2018. Basics of Bidirectionalism. (Aug.2018). Retrieved from https:\/\/pigworker.wordpress.com\/2018\/08\/06\/basics-of-bidirectionalism\/Blog post."},{"key":"e_1_3_3_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_3_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167089"},{"key":"e_1_3_3_56_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000282"},{"key":"e_1_3_3_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575685"},{"key":"e_1_3_3_58_1","volume-title":"Inductive-inductive Definitions","author":"Forsberg Fredrik Nordvall","year":"2013","unstructured":"Fredrik Nordvall Forsberg. 2013. Inductive-inductive Definitions. Ph. D. Dissertation. Swansea University."},{"key":"e_1_3_3_59_1","volume-title":"Towards a Practical Programming Language Based on Dependent Type Theory","author":"Norell Ulf","year":"2007","unstructured":"Ulf Norell. 2007. Towards a Practical Programming Language Based on Dependent Type Theory. Ph. D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg, Sweden. Retrieved from http:\/\/www.cs.chalmers.se\/ulfn\/papers\/thesis.html"},{"key":"e_1_3_3_60_1","unstructured":"Kristian Knudsen Olesen. 2021. Extracting certified futhark code from Coq. (2021)."},{"key":"e_1_3_3_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80002-5"},{"key":"e_1_3_3_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005113"},{"key":"e_1_3_3_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_3_64_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_3_3_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"e_1_3_3_66_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000044"},{"key":"e_1_3_3_67_1","unstructured":"Gert Smolka. 2015. Confluence and Normalization in Reduction Systems. (2015). Retrieved from https:\/\/www.ps.uni-saarland.de\/courses\/sem-ws15\/ars.pdfLecture Notes."},{"key":"e_1_3_3_68_1","volume-title":"D\u00e9veloppement Modulaire De th\u00e9ories et Gestion de L\u2019espace de Nom Pour L\u2019assistant de Preuve Coq.","author":"Soubiran Elie","year":"2010","unstructured":"Elie Soubiran. 2010. D\u00e9veloppement Modulaire De th\u00e9ories et Gestion de L\u2019espace de Nom Pour L\u2019assistant de Preuve Coq. Theses. Ecole Polytechnique X. Retrieved from https:\/\/theses.hal.science\/tel-00679201"},{"key":"e_1_3_3_69_1","volume-title":"Un environnement Pour la Programmation Avec Types D\u00e9pendants","author":"Sozeau Matthieu","year":"2008","unstructured":"Matthieu Sozeau. 2008. Un environnement Pour la Programmation Avec Types D\u00e9pendants. Ph. D. Dissertation. Universit\u00e9 Paris 11, Orsay, France."},{"key":"e_1_3_3_70_1","unstructured":"Matthieu Sozeau Abhishek Anand Simon Boulier Cyril Cohen Yannick Forster Fabian Kunze Gregory Malecha Nicolas Tabareau and Th\u00e9o Winterhalter. 2019a. The MetaCoq Project. (June2019). Retrieved from https:\/\/hal.inria.fr\/hal-02167423(submitted)."},{"key":"e_1_3_3_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_3_3_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_3_3_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_32"},{"key":"e_1_3_3_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103723"},{"key":"e_1_3_3_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80045-8"},{"key":"e_1_3_3_76_1","unstructured":"Enrico Tassi. 2018. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi \u03bbProlog dialect). (Jan.2018). Retrieved from https:\/\/hal.inria.fr\/hal-01637063working paper or preprint."},{"key":"e_1_3_3_77_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2019.29"},{"key":"e_1_3_3_78_1","unstructured":"The Coq Development Team. 2016. The Coq Proof Assistant version 8.5. Retrieved from https:\/\/coq.inria.fr\/distrib\/V8.5pl3\/refman\/"},{"key":"e_1_3_3_79_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7313584"},{"key":"e_1_3_3_80_1","first-page":"30","volume-title":"Consistency of the Predicative Calculus of Cumulative Inductive Constructions","author":"Timany Amin","year":"2017","unstructured":"Amin Timany and Matthieu Sozeau. 2017. Consistency of the Predicative Calculus of Cumulative Inductive Constructions. Research Report RR-9105. KU Leuven, Belgium ; Inria Paris. 30 pages. Retrieved from https:\/\/hal.inria.fr\/hal-01615123"},{"key":"e_1_3_3_81_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2018.29"},{"key":"e_1_3_3_82_1","article-title":"Views . A Way for elegant definitions and efficient representations to coexist","author":"Wadler Philip","year":"1985","unstructured":"Philip Wadler. 1985. Views . A Way for elegant definitions and efficient representations to coexist. Oxford University. Retrieved from http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/view\/view.ps","journal-title":"Oxford University"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3706056","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3706056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:13Z","timestamp":1750295893000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3706056"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,27]]},"references-count":81,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,2,28]]}},"alternative-id":["10.1145\/3706056"],"URL":"https:\/\/doi.org\/10.1145\/3706056","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,27]]},"assertion":[{"value":"2023-04-21","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-13","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}