×

The MetaCoq project. (English) Zbl 1468.68075

Summary: The MetaCoq project aims to provide a certified meta-programming environment in Coq. It builds on Template-Coq, a plugin for Coq originally implemented by G. Malecha [Extensible proof engineering in intensional type theory. Cambridge, MA: Harvard University, Graduate School of Arts & Sciences (PhD Thesis) (2015)], which provided a reifier for Coq terms and global declarations, as represented in the Coq kernel, as well as a denotation command. Recently, it was used in the CertiCoq certified compiler project, as its front-end language, to derive parametricity properties. However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq’s type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire polymorphic calculus of cumulative inductive constructions, as implemented by Coq, including the kernel’s declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq’s logical environment. We demonstrate how this setup allows Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation and a certified extraction to call-by-value \(\lambda \)-calculus. We also advocate the use of MetaCoq as a foundation for higher-level tools.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abel, A.; Öhman, J.; Vezzosi, A., Decidability of conversion for type theory in type theory, PACMPL, 2, POPL, 23:1-23:29 (2018) · doi:10.1145/3158111
[2] Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: POPL’16, pp. 18-29, ACM, New York, NY, USA (2016) 10.1145/2837614.2837638 · Zbl 1347.68045
[3] Anand, A., Morrisett, G.: Revisiting parametricity: inductives and uniformity of propositions. In: CoqPL’18. Los Angeles, CA, USA (2018)
[4] 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)
[5] Anand, A., Boulier, S., Cohen, C., Sozeau, M., Tabareau, N.: Towards certified meta-programming with typed template-Coq. In: ITP 2018—9th Conference on Interactive Theorem Proving. LNCS, vol. 10895, pp. 20-39. Springer, Oxford, United Kingdom (2018) 10.1007/978-3-319-94821-8_2, https://hal.archives-ouvertes.fr/hal-01809681 · Zbl 1468.68071
[6] Annenkov, D., Spitters, B.: Towards a smart contract verification framework in coq. CoRR abs/1907.10674. arXiv:1907.10674 (2019)
[7] Armand, M., Grégoire, B., Spiwack, A., Théry, L.: Extending Coq with imperative features and its application to SAT verification. In: Kaufmann, M., Paulson, L.C., (eds.) Interactive Theorem Proving, pp. 83-98. Springer (2010) · Zbl 1291.68318
[8] 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-12, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10895. Springer (2018). 10.1007/978-3-319-94821-8 · Zbl 1391.68001
[9] Barras, B.: Auto-validation d’un système de preuves avec familles inductives. Thèse de doctorat, Université Paris 7. http://pauillac.inria.fr/ barras/publi/these_barras.ps.gz (1999)
[10] Bernardy, JP; Jansson, P.; Paterson, R., Proofs for free: parametricity for dependent types, J. Funct. Program., 22, 2, 107-152 (2012) · Zbl 1271.68076 · doi:10.1017/S0956796812000056
[11] Boespflug, M., Dénès, M., Grégoire, B.: Full reduction at full throttle. In: International Conference on Certified Programs and Proofs, pp. 362-377. Springer (2011)
[12] Boulier, S., Pédrot, P.M., Tabareau, N.: The next 700 syntactical models of type theory. In: CPP’17, pp. 182-194. ACM, Paris, France (2017)
[13] Carette, J., Farmer, W.M., Laskowski, P.: HOL light QE. In: Avigad, Mahboubi (eds.) International Conference on Interactive Theorem Proving, pp. 215-234 (2018). 10.1007/978-3-319-94821-8_13 · Zbl 1511.68307
[14] Chapman, J., Type theory should eat itself, Electron. Notes Theor. Comput. Sci., 228, 21-36 (2009) · Zbl 1337.68057 · doi:10.1016/j.entcs.2008.12.114
[15] Chlipala, A., Certified Programming with Dependent Types (2011), Cambridge: MIT Press, Cambridge
[16] Christiansen, D., Brady, E.: Elaborator reflection: extending Idris in Idris. In: ICFP’16, p. 284 (2016) · Zbl 1361.68035
[17] Cormen, TH; Leiserson, CE; Rivest, RL; Stein, C., Introduction to algorithms (2009), Cambridge: MIT Press, Cambridge · Zbl 1187.68679
[18] Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ACM, ICFP’13 (2013). 10.1145/2500365.2500575 · Zbl 1323.68109
[19] Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. In: Proceedings of the 22st ACM SIGPLAN Conference on Functional Programming (ICFP 2017), pp. 34:1-34:29. ACM Press, Oxford, UK (2017)
[20] Feferman, S.: Typical Ambiguity: Trying to Have Your Cake and Eat it Too, Invited Lecture for the Conference, One Hundred Years of Russell’s Paradox (2001) · Zbl 1060.03009
[21] 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)
[22] Forster, Y., Kunze, F.: A certifying extraction with time bounds from Coq to call-by-value Lambda calculus. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, Leibniz International Proceedings in Informatics (LIPIcs), vol. 141, pp. 17:1-17:19 (2019) · Zbl 07649966
[23] Forster, Y., Smolka, G.: Weak call-by-value lambda calculus as a model of computation in Coq. In: ITP 2017, pp. 189-206. Springer (2017) · Zbl 1468.68322
[24] Grégoire, B.; Leroy, X., A compiled implementation of strong reduction, ACM, 37, 235-246 (2002) · Zbl 1322.68053
[25] Gross, J., Erbsen, A., Chlipala, A.: Reification by parametricity—fast setup for proof by reflection, in two lines of ltac. In: Avigad and Mahboubi (eds.) International Conference on Interactive Theorem Proving, pp. 289-305 (2018) 10.1007/978-3-319-94821-8_17 · Zbl 1511.68311
[26] Herbelin, H.: Type inference with algebraic universes in the calculus of inductive constructions. In: TYPES’05. http://pauillac.inria.fr/ herbelin/publis/univalgcci.pdf manuscript (2005)
[27] Jaber, G., Lewertowski, G., Pédrot, P.M., Sozeau, M., Tabareau, N.: The definitional side of the forcing. In: LICS’16, pp. 367-376. New York, NY, USA (2016). 10.1145/2933575.2935320 · Zbl 1394.68063
[28] 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-180. Springer (2013) · Zbl 1405.68060
[29] Kaiser, J.; Ziliani, B.; Krebbers, R.; Régis-Gianas, Y.; Dreyer, D., Mtac2: typed tactics for backward reasoning in Coq, PACMPL 2(ICFP), 2, 78:1-78:31 (2018) · doi:10.1145/3236773
[30] Keller, C., Lasson, M.: Parametricity in an impredicative sort. CoRR abs/1209.6336. arXiv:1209.6336 (2012) · Zbl 1252.68259
[31] 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). 10.1016/j.entcs.2014.10.013 · Zbl 1337.03016
[32] Malecha, G., Bengtson, J.: Extensible and efficient automation through reflective tactics. In: ESOP 2016 (2016). 10.1007/978-3-662-49498-1_21, · Zbl 1335.68234
[33] 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)
[34] Mogensen, TÆ, Efficient self-interpretations in lambda calculus, J. Funct. Program., 2, 3, 345-363 (1992) · Zbl 0817.68051 · doi:10.1017/S0956796800000423
[35] Mullen, E.; Pernsteiner, S.; Wilcox, JR; Tatlock, Z.; Grossman, D., Œuf: minimizing the coq extraction TCB, Proc. CPP, 2018, 172-185 (2018) · doi:10.1145/3167089
[36] Pédrot, P., Tabareau, N.: An effectful way to eliminate addiction to dependence. In: LICS’17, pp. 1-12. Reykjavik, Iceland (2017). 10.1109/LICS.2017.8005113,
[37] Pédrot, P.M.: Ltac2: tactical warfare. CoqPL 2019 (2019)
[38] Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513-523 (1983)
[39] Russell, B., Mathematical logic as based on the theory of types, Am. J. Math., 30, 3, 222-262 (1908) · JFM 39.0085.03 · doi:10.2307/2272708
[40] Sheard, T.; Jones, SP, Template meta-programming for haskell, SIGPLAN Not., 37, 12, 60-75 (2002) · doi:10.1145/636517.636528
[41] Sheard, T., Jones, S.P.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, Haskell’02, pp. 1-16. ACM, New York, NY, USA (2002b). 10.1145/581690.581691
[42] Sozeau, M.: Program-ing Finger Trees in Coq. In: ICFP’07. ACM, pp. 13-24, New York, NY, USA (2007). 10.1145/1291151.1291156 · Zbl 1291.68157
[43] Sozeau, M.; Mangin, C., Equations reloaded: high-level dependently-typed programming and proving in Coq, PACMPL, 3, ICFP, 86-115 (2019) · doi:10.1145/3341690
[44] Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: PEPM’97, pp. 203-217. ACM, New York, NY, USA (1997). 10.1145/258993.259019 · Zbl 0949.68047
[45] Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture, pp. 347-359. ACM Press, New York City (1989)
[46] Van der Walt, P., Swierstra, W.: Engineering proof by reflection in Agda. In: Implementation and Application of Functional Languages. Springer (2013)
[47] 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)
[48] Ziliani, B.; Sozeau, M., A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading, J. Funct. Program., 27, e10 (2017) · Zbl 1418.68185 · doi:10.1017/S0956796817000028
[49] Ziliani, B.; Dreyer, D.; Krishnaswami, NR; Nanevski, A.; Vafeiadis, V., Mtac: A monad for typed tactic programming in Coq, J. Funct. Program. (2015) · Zbl 1420.68189 · doi:10.1017/S0956796815000118
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.