{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T21:56:58Z","timestamp":1784239018438,"version":"3.55.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2020,2,18]],"date-time":"2020-02-18T00:00:00Z","timestamp":1581984000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,2,18]],"date-time":"2020-02-18T00:00:00Z","timestamp":1581984000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"ERC starting grant","award":["64399"],"award-info":[{"award-number":["64399"]}]},{"name":"NSF","award":["CCF-1407794"],"award-info":[{"award-number":["CCF-1407794"]}]},{"name":"NSF","award":["CCF-1521602"],"award-info":[{"award-number":["CCF-1521602"]}]},{"name":"NSF","award":["CCF-1646417"],"award-info":[{"award-number":["CCF-1646417"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s10817-019-09540-0","type":"journal-article","created":{"date-parts":[[2020,2,18]],"date-time":"2020-02-18T19:02:40Z","timestamp":1582052560000},"page":"947-999","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":57,"title":["The MetaCoq Project"],"prefix":"10.1007","volume":"64","author":[{"given":"Matthieu","family":"Sozeau","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Abhishek","family":"Anand","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon","family":"Boulier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cyril","family":"Cohen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yannick","family":"Forster","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fabian","family":"Kunze","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gregory","family":"Malecha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Th\u00e9o","family":"Winterhalter","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,2,18]]},"reference":[{"issue":"POPL","key":"9540_CR1","doi-asserted-by":"publisher","first-page":"23:1","DOI":"10.1145\/3158111","volume":"2","author":"A Abel","year":"2018","unstructured":"Abel, A., \u00d6hman, J., Vezzosi, A.: Decidability of conversion for type theory in type theory. PACMPL 2(POPL), 23:1\u201323:29 (2018). https:\/\/doi.org\/10.1145\/3158111","journal-title":"PACMPL"},{"key":"9540_CR2","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: POPL\u201916, pp. 18\u201329, ACM, New York, NY, USA (2016) https:\/\/doi.org\/10.1145\/2837614.2837638","DOI":"10.1145\/2837614.2837638"},{"key":"9540_CR3","unstructured":"Anand, A., Morrisett, G.: Revisiting parametricity: inductives and uniformity of propositions. In: CoqPL\u201918. Los Angeles, CA, USA (2018)"},{"key":"9540_CR4","unstructured":"Anand, A., Appel, A., Morrisett, G., Paraskevopoulou, Z., Pollack, R., Belanger, O.S., Sozeau, M., Weaver, M.: CertiCoq: a verified compiler for Coq. In: CoqPL. Paris, France. http:\/\/conf.researchr.org\/event\/CoqPL-2017\/main-certicoq-a-verified-compiler-for-coq (2017)"},{"key":"9540_CR5","doi-asserted-by":"publisher","unstructured":"Anand, A., Boulier, S., Cohen, C., Sozeau, M., Tabareau, N.: Towards certified meta-programming with typed template-Coq. In: ITP 2018\u20149th Conference on Interactive Theorem Proving. LNCS, vol. 10895, pp. 20\u201339. Springer, Oxford, United Kingdom (2018) https:\/\/doi.org\/10.1007\/978-3-319-94821-8_2, https:\/\/hal.archives-ouvertes.fr\/hal-01809681","DOI":"10.1007\/978-3-319-94821-8_2"},{"key":"9540_CR6","doi-asserted-by":"crossref","unstructured":"Annenkov, D., Spitters, B.: Towards a smart contract verification framework in coq. CoRR abs\/1907.10674. arXiv:1907.10674 (2019)","DOI":"10.1145\/3372885.3373829"},{"key":"9540_CR7","doi-asserted-by":"crossref","unstructured":"Armand, M., Gr\u00e9goire, B., Spiwack, A., Th\u00e9ry, L.: Extending Coq with imperative features and its application to SAT verification. In: Kaufmann, M., Paulson, L.C., (eds.) Interactive Theorem Proving, pp. 83\u201398. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_8"},{"key":"9540_CR8","doi-asserted-by":"publisher","unstructured":"Avigad, J., Mahboubi, A.: Interactive theorem proving. In: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9\u201312, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10895. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8","DOI":"10.1007\/978-3-319-94821-8"},{"key":"9540_CR9","unstructured":"Barras, B.: Auto-validation d\u2019un syst\u00e8me de preuves avec familles inductives. Th\u00e8se de doctorat, Universit\u00e9 Paris\u00a07. http:\/\/pauillac.inria.fr\/~barras\/publi\/these_barras.ps.gz (1999)"},{"issue":"2","key":"9540_CR10","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1017\/S0956796812000056","volume":"22","author":"JP Bernardy","year":"2012","unstructured":"Bernardy, J.P., Jansson, P., Paterson, R.: Proofs for free: parametricity for dependent types. J. Funct. Program. 22(2), 107\u2013152 (2012)","journal-title":"J. Funct. Program."},{"key":"9540_CR11","doi-asserted-by":"crossref","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full reduction at full throttle. In: International Conference on Certified Programs and Proofs, pp. 362\u2013377. Springer (2011)","DOI":"10.1007\/978-3-642-25379-9_26"},{"key":"9540_CR12","doi-asserted-by":"crossref","unstructured":"Boulier, S., P\u00e9drot, P.M., Tabareau, N.: The next 700 syntactical models of type theory. In: CPP\u201917, pp. 182\u2013194. ACM, Paris, France (2017)","DOI":"10.1145\/3018610.3018620"},{"key":"9540_CR13","doi-asserted-by":"publisher","unstructured":"Carette, J., Farmer, W.M., Laskowski, P.: HOL light QE. In: Avigad, Mahboubi (eds.) International Conference on Interactive Theorem Proving, pp. 215\u2013234 (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_13","DOI":"10.1007\/978-3-319-94821-8_13"},{"key":"9540_CR14","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2008.12.114","volume":"228","author":"J Chapman","year":"2009","unstructured":"Chapman, J.: Type theory should eat itself. Electron. Notes Theor. Comput. Sci. 228, 21\u201336 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2008.12.114","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9540_CR15","volume-title":"Certified Programming with Dependent Types","author":"A Chlipala","year":"2011","unstructured":"Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2011)"},{"key":"9540_CR16","doi-asserted-by":"crossref","unstructured":"Christiansen, D., Brady, E.: Elaborator reflection: extending Idris in Idris. In: ICFP\u201916, p. 284 (2016)","DOI":"10.1145\/3022670.2951932"},{"key":"9540_CR17","volume-title":"Introduction to algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms. MIT Press, Cambridge (2009)"},{"key":"9540_CR18","doi-asserted-by":"publisher","unstructured":"Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ACM, ICFP\u201913 (2013). https:\/\/doi.org\/10.1145\/2500365.2500575","DOI":"10.1145\/2500365.2500575"},{"key":"9540_CR19","doi-asserted-by":"crossref","unstructured":"Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de\u00a0Moura, L.: A metaprogramming framework for formal verification. In: Proceedings of the 22st ACM SIGPLAN Conference on Functional Programming (ICFP 2017), pp. 34:1\u201334:29. ACM Press, Oxford, UK (2017)","DOI":"10.1145\/3110278"},{"key":"9540_CR20","unstructured":"Feferman, S.: Typical Ambiguity: Trying to Have Your Cake and Eat it Too, Invited Lecture for the Conference, One Hundred Years of Russell\u2019s Paradox (2001)"},{"key":"9540_CR21","unstructured":"Forster, Y., Kunze, F.: Verified Extraction from Coq to a Lambda-calculus. In: Coq Workshop 2016. https:\/\/www.ps.uni-saarland.de\/~forster\/coq-workshop-16\/abstract-coq-ws-16.pdf (2016)"},{"key":"9540_CR22","unstructured":"Forster, Y., Kunze, F.: A certifying extraction with time bounds from Coq to call-by-value Lambda calculus. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019), Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, Leibniz International Proceedings in Informatics (LIPIcs), vol. 141, pp. 17:1\u201317:19 (2019)"},{"key":"9540_CR23","doi-asserted-by":"crossref","unstructured":"Forster, Y., Smolka, G.: Weak call-by-value lambda calculus as a model of computation in Coq. In: ITP 2017, pp. 189\u2013206. Springer (2017)","DOI":"10.1007\/978-3-319-66107-0_13"},{"key":"9540_CR24","first-page":"235","volume":"37","author":"B Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. ACM 37, 235\u2013246 (2002)","journal-title":"ACM"},{"key":"9540_CR25","doi-asserted-by":"publisher","unstructured":"Gross, J., Erbsen, A., Chlipala, A.: Reification by parametricity\u2014fast setup for proof by reflection, in two lines of ltac. In: Avigad and Mahboubi (eds.) International Conference on Interactive Theorem Proving, pp. 289\u2013305 (2018) https:\/\/doi.org\/10.1007\/978-3-319-94821-8_17","DOI":"10.1007\/978-3-319-94821-8_17"},{"key":"9540_CR26","unstructured":"Herbelin, H.: Type inference with algebraic universes in the calculus of inductive constructions. In: TYPES\u201905. http:\/\/pauillac.inria.fr\/~herbelin\/publis\/univalgcci.pdf manuscript (2005)"},{"key":"9540_CR27","doi-asserted-by":"publisher","unstructured":"Jaber, G., Lewertowski, G., P\u00e9drot, P.M., Sozeau, M., Tabareau, N.: The definitional side of the forcing. In: LICS\u201916, pp. 367\u2013376. New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2933575.2935320","DOI":"10.1145\/2933575.2935320"},{"key":"9540_CR28","doi-asserted-by":"crossref","unstructured":"Jansen, J.M.: Programming in the $$\\lambda $$-calculus: from Church to Scott and back. In: The Beauty of Functional Code. LNCS, vol .8106, pp. 168\u2013180. Springer (2013)","DOI":"10.1007\/978-3-642-40355-2_12"},{"key":"9540_CR29","doi-asserted-by":"publisher","first-page":"78:1","DOI":"10.1145\/3236773","volume":"2","author":"J Kaiser","year":"2018","unstructured":"Kaiser, J., Ziliani, B., Krebbers, R., R\u00e9gis-Gianas, Y., Dreyer, D.: Mtac2: typed tactics for backward reasoning in Coq. PACMPL 2(ICFP) 2, 78:1\u201378:31 (2018). https:\/\/doi.org\/10.1145\/3236773","journal-title":"PACMPL 2(ICFP)"},{"key":"9540_CR30","unstructured":"Keller, C., Lasson, M.: Parametricity in an impredicative sort. CoRR abs\/1209.6336. arXiv:1209.6336 (2012)"},{"key":"9540_CR31","doi-asserted-by":"publisher","unstructured":"Lasson, M.: Canonicity of weak $$\\omega $$-groupoid laws using parametricity theory. In: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX) (2014). https:\/\/doi.org\/10.1016\/j.entcs.2014.10.013","DOI":"10.1016\/j.entcs.2014.10.013"},{"key":"9540_CR32","doi-asserted-by":"publisher","unstructured":"Malecha, G., Bengtson, J.: Extensible and efficient automation through reflective tactics. In: ESOP 2016 (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_21,","DOI":"10.1007\/978-3-662-49498-1_21"},{"key":"9540_CR33","unstructured":"Malecha, G.M.: Extensible proof engineering in intensional type theory. PhD thesis, Harvard University. http:\/\/gmalecha.github.io\/publication\/2015\/02\/01\/extensible-proof-engineering-in-intensional-type-theory.html (2014)"},{"issue":"3","key":"9540_CR34","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1017\/S0956796800000423","volume":"2","author":"T\u00c6 Mogensen","year":"1992","unstructured":"Mogensen, T.\u00c6.: Efficient self-interpretations in lambda calculus. J. Funct. Program. 2(3), 345\u2013363 (1992)","journal-title":"J. Funct. Program."},{"key":"9540_CR35","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/3167089","volume":"2018","author":"E Mullen","year":"2018","unstructured":"Mullen, E., Pernsteiner, S., Wilcox, J.R., Tatlock, Z., Grossman, D.: \u0152uf: minimizing the coq extraction TCB. Proc. CPP 2018, 172\u2013185 (2018). https:\/\/doi.org\/10.1145\/3167089","journal-title":"Proc. CPP"},{"key":"9540_CR36","doi-asserted-by":"publisher","unstructured":"P\u00e9drot, P., Tabareau, N.: An effectful way to eliminate addiction to dependence. In: LICS\u201917, pp. 1\u201312. Reykjavik, Iceland (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005113,","DOI":"10.1109\/LICS.2017.8005113"},{"key":"9540_CR37","unstructured":"P\u00e9drot, P.M.: Ltac2: tactical warfare. CoqPL 2019 (2019)"},{"key":"9540_CR38","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513\u2013523 (1983)"},{"issue":"3","key":"9540_CR39","doi-asserted-by":"publisher","first-page":"222","DOI":"10.2307\/2272708","volume":"30","author":"B Russell","year":"1908","unstructured":"Russell, B.: Mathematical logic as based on the theory of types. Am. J. Math. 30(3), 222\u2013262 (1908). https:\/\/doi.org\/10.2307\/2272708","journal-title":"Am. J. Math."},{"issue":"12","key":"9540_CR40","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/636517.636528","volume":"37","author":"T Sheard","year":"2002","unstructured":"Sheard, T., Jones, S.P.: Template meta-programming for haskell. SIGPLAN Not. 37(12), 60\u201375 (2002a). https:\/\/doi.org\/10.1145\/636517.636528","journal-title":"SIGPLAN Not."},{"key":"9540_CR41","doi-asserted-by":"publisher","unstructured":"Sheard, T., Jones, S.P.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, Haskell\u201902, pp. 1\u201316. ACM, New York, NY, USA (2002b). https:\/\/doi.org\/10.1145\/581690.581691","DOI":"10.1145\/581690.581691"},{"key":"9540_CR42","doi-asserted-by":"publisher","unstructured":"Sozeau, M.: Program-ing Finger Trees in Coq. In: ICFP\u201907. ACM, pp. 13\u201324, New York, NY, USA (2007). https:\/\/doi.org\/10.1145\/1291151.1291156","DOI":"10.1145\/1291151.1291156"},{"issue":"ICFP","key":"9540_CR43","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3341690","volume":"3","author":"M Sozeau","year":"2019","unstructured":"Sozeau, M., Mangin, C.: Equations reloaded: high-level dependently-typed programming and proving in Coq. PACMPL 3(ICFP), 86\u2013115 (2019). https:\/\/doi.org\/10.1145\/3341690","journal-title":"PACMPL"},{"key":"9540_CR44","doi-asserted-by":"publisher","unstructured":"Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: PEPM\u201997, pp. 203\u2013217. ACM, New York, NY, USA (1997). https:\/\/doi.org\/10.1145\/258993.259019","DOI":"10.1145\/258993.259019"},{"key":"9540_CR45","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture, pp. 347\u2013359. ACM Press, New York City (1989)","DOI":"10.1145\/99370.99404"},{"key":"9540_CR46","doi-asserted-by":"crossref","unstructured":"Van\u00a0der Walt, P., Swierstra, W.: Engineering proof by reflection in Agda. In: Implementation and Application of Functional Languages. Springer (2013)","DOI":"10.1007\/978-3-642-41582-1_10"},{"key":"9540_CR47","unstructured":"Zaliva, V., Sozeau, M.: Reification of shallow-embedded DSLs in Coq with automated verification. In: CoqPL, Cascais, Portugal. http:\/\/www.crocodile.org\/lord\/vzaliva-CoqPL19.pdf (2019)"},{"key":"9540_CR48","doi-asserted-by":"publisher","first-page":"e10","DOI":"10.1017\/S0956796817000028","volume":"27","author":"B Ziliani","year":"2017","unstructured":"Ziliani, B., Sozeau, M.: A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. J. Funct. Program. 27, e10 (2017). https:\/\/doi.org\/10.1017\/S0956796817000028","journal-title":"J. Funct. Program."},{"key":"9540_CR49","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000118","author":"B Ziliani","year":"2015","unstructured":"Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: A monad for typed tactic programming in Coq. J. Funct. Program. (2015). https:\/\/doi.org\/10.1017\/S0956796815000118","journal-title":"J. Funct. Program."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09540-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09540-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09540-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,15]],"date-time":"2022-10-15T22:28:29Z","timestamp":1665872909000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09540-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,18]]},"references-count":49,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["9540"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09540-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,2,18]]},"assertion":[{"value":"30 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 December 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 February 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}