×

Mtac: a monad for typed tactic programming in Coq. (English) Zbl 1420.68189

Summary: Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers.
We present Mtac, a lightweight but powerful extension to Coq that supports dependently typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Allen, S. F., Constable, R. L., Howe, D. J. & Aitken, W. E. (1990) The semantics of reflected proof. In IEEE Symposium on Logic in Computer Science (LICS). New York: IEEE.
[2] Armand, M., Grégoire, B., Spiwack, A. & Théry, L. (2010) Extending Coq with imperative features and its application to SAT verification. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer. · Zbl 1291.68318
[3] Artëmov, S. N. (1999) On explicit reflection in theorem proving and formal verification. In Conference on Automated Deduction (CADE). Berlin: Springer. · Zbl 0937.03015
[4] Asperti, A., Ricciotti, W., Sacerdoti Coen, C. & Tassi, E. (2009) A compact kernel for the calculus of inductive constructions. Sadhana34(1), 71-144. doi:10.1007/s12046-009-0003-32547328 · Zbl 1196.68221 · doi:10.1007/s12046-009-0003-3
[5] Baker, H. G. (1991) Shallow binding makes functional arrays fast. SIGPLAN Not.26(8), 145-147.
[6] Barendregt, H. & Geuvers, H. (2001) Proof-assistants using dependent type systems. In Handbook of Automated Reasoning, Robinson, A. & Voronkov, A. (eds), Elsevier Science Publishers B. V., pp. 1149-1238 doi:10.1016/B978-044450813-3/50020-5 · Zbl 1005.03011
[7] Bertot, Y. & Castéran, P. (2004) Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer. · Zbl 1069.68095
[8] Boutin, S. (1997) Using reflection to build efficient and certified decision procedures. In International Symposium on Theoretical Aspects of Computer Software (TACS). Berlin: Springer.
[9] Cave, A. & Pientka, B. (2012) Programming with binders and indexed data-types. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM. · Zbl 1321.68141
[10] Chlipala, A. (2011a) Certified Programming with Dependent Types. MIT Press. http://adam.chlipala.net/cpdt/. · Zbl 1288.68001
[11] Chlipala, A. (2011b) Mostly-automated verification of low-level programs in computational separation logic. In ACM Conference on Programming Languages Design and Implementation (PLDI), pp. 234-245. New York: ACM.
[12] Claret, G., Del Carmen González Huesca, L., Régis-Gianas, Y. & Ziliani, B. (2013) Lightweight proof by reflection using a posteriori simulation of effectful computation. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer. · Zbl 1317.68205
[13] Constable, R. L. (1992) Metalevel programming in constructive type theory. In Programming and Mathematical Method, Broy, M. (ed), NATO ASI Series, vol. 88. New York: Springer-Verlag, pp. 45-93. doi:10.1007/978-3-642-77572-7_6
[14] Devriese, D. & Piessens, F. (2013) Typed syntactic meta-programming. In International Conference on Functional Programming (ICFP). New York: ACM. · Zbl 1323.68109
[15] Gonthier, G. (2008) Formal proof-the four-color theorem. Not. AMS55(11), 1382-93. · Zbl 1195.05026
[16] Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Leroux, S., Mahboubi, A., O’Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E. & Théry, L. (2013b) A machine-checked proof of the odd order theorem. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer. · Zbl 1317.68211
[17] Gonthier, G., Mahboubi, A. & Tassi, E. (2008) A Small Scale Reflection Extension for the Coq System. Technical Report, INRIA.
[18] Gonthier, G., Ziliani, B., Nanevski, A. & Dreyer, D. (2013a) How to make ad hoc proof automation less ad hoc. J. Funct. Program. (JFP)23(4), 357-401. doi:10.1017/S09567968130000513148852 · Zbl 1314.68281
[19] Grégoire, B. & Leroy, X. (2002) A compiled implementation of strong reduction. In International Conference on Functional Programming (ICFP). New York: ACM. · Zbl 1322.68053
[20] Harper, R., Honsell, F. & Plotkin, G. (1993) A framework for defining logics. J. ACM (JACM)40(1), 143-184. doi:10.1145/138027.138060 · Zbl 0778.03004 · doi:10.1145/138027.138060
[21] Harrison, J. (1995) Metatheory and Reflection in Theorem Proving: A Survey and Critique. Technical Report CRC-053. SRI Cambridge, Millers Yard, Cambridge, UK.
[22] Howe, D. J. (1992) Reflecting the semantics of reflected proof. In Proof Theory. Cambridge University Press, pp. 227-250. · Zbl 0808.03007
[23] Hur, C.-K., Neis, G., Dreyer, D. & Vafeiadis, V. (2013) The power of parameterization in coinductive proof. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM. · Zbl 1301.68220
[24] Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H. & Winwood, S. (2010) seL4: Formal verification of an operating-system kernel. Commun. ACM (CACM)53(6), 107-115.
[25] Launchbury, J. & Peyton Jones, S. L. (1994) Lazy functional state threads. In ACM Conference on Programming Languages Design and Implementation (PLDI). New York: ACM.
[26] Leroy, X. (2009) Formal verification of a realistic compiler. Commun. ACM (CACM)52(7), 107-115. doi:10.1145/1538788.1538814 · doi:10.1145/1538788.1538814
[27] Malecha, G. & Bengtson, J. (2015) Rtac: A fully reflective tactic language. In International Workshop on Coq for PL (CoqPL).
[28] Malecha, G., Chlipala, A. & Braibant, T. (2014) Compositional computational reflection. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer. · Zbl 1416.68171
[29] Mendler, N. P. (1991) Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Log.51(1-2), 159-172. doi:10.1016/0168-0072(91)90069-X1100500 · Zbl 0719.03008 · doi:10.1016/0168-0072(91)90069-X
[30] Miculan, M. & Paviotti, M. (2012) Synthesis of distributed mobile programs using monadic types in coq. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer. · Zbl 1360.68760
[31] Miller, D. (1991) Unification of simply typed lamda-terms as logic programming. In International Conference on Logic Programming (ICLP). Berlin: Springer.
[32] Nanevski, A. (2002) Meta-programming with names and necessity. In International Conference on Functional Programming (ICFP). New York: ACM. · Zbl 1322.68045
[33] Nanevski, A., Morrisett, G. & Birkedal, L. (2008b) Hoare type theory, polymorphism and separation. J. Funct. Program. (JFP)18(5-6), 865-911. doi:10.1017/S09567968080069532472476 · Zbl 1155.68354
[34] Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P. & Birkedal, L. (2008c) Ynot: Dependent types for imperative programs. In International Conference on Functional Programming (ICFP). New York: ACM. · Zbl 1323.68142
[35] Nanevski, A., Pfenning, F. & Pientka, B. (2008a) Contextual modal type theory. ACM Trans. Comput. Log. (TOCL)9(3), 23:1-23:49.2426371 · Zbl 1367.03060
[36] Nanevski, A., Vafeiadis, V. & Berdine, J. (2010) Structuring the verification of heap-manipulating programs. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM. · Zbl 1312.68065
[37] Pientka, B. (2008) A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM. · Zbl 1295.68068
[38] Pientka, B. & Dunfield, J. (2008) Programming with proofs and explicit contexts. In International Symposium on Principles and Practice of Declarative Programming (PPDP). New York: ACM. · Zbl 1291.68366
[39] Pollack, R. (1995) On extensibility of proof checkers. In TYPES. Berlin: Springer.
[40] Poswolsky, A. & Schürmann, C. (2009) System description: Delphin – a functional programming language for deductive systems. In Electron. Notes Theor. Comput. Sci. (ENTCS)228, 113-120. doi:10.1016/j.entcs.2008.12.120
[41] Sacerdoti Coen, C. (2004) Mathematical Knowledge Management and Interactive Theorem Proving. PhD Thesis, University of Bologna. · Zbl 1108.68601
[42] Saïbi, A. (1997) Typing algorithm in type theory with inheritance. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM.
[43] Schürmann, C., Poswolsky, A. & Sarnat, J. (2005) The ∇-calculus. Functional programming with higher-order encodings. In International Conference on Typed Lambda Calculi and Applications (TLCA). Berlin: Springer. · Zbl 1114.68030
[44] Ševčík, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S. & Sewell, P. (2013) CompCertTSO: A verified compiler for relaxed-memory concurrency. J. ACM (JACM)60(3), 22:1-22:50.3078709 · Zbl 1281.68072
[45] Sozeau, M. (2007) Subset coercions in Coq. In TYPES. Berlin: Springer. · Zbl 1178.68531
[46] Sozeau, M. & Oury, N. (2008) First-class type classes. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs). Berlin: Springer. · Zbl 1165.68475
[47] Stampoulis, A. & Shao, Z. (2010) VeriML: Typed computation of logical terms inside a language with effects. In International Conference on Functional Programming (ICFP). New York: ACM. · Zbl 1323.68384
[48] Stampoulis, A. & Shao, Z. (2012) Static and user-extensible proof checking. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM. · Zbl 1321.68204
[49] . (2012) The Coq Proof Assistant Reference Manual-Version V8.4.
[50] Vafeiadis, V. (2013) Adjustable references. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer. · Zbl 1317.68234
[51] Van Der Walt, P. & Swierstra, W. (2013) Engineering proof by reflection in Agda. In Implementation and Application of Functional Languages (IFL).
[52] Ziliani, B., Dreyer, D., Krishnaswami, N. R., Nanevski, A. & Vafeiadis, V. (2013) Mtac: A monad for typed tactic programming in Coq. In International Conference on Functional Programming (ICFP). New York: ACM. · Zbl 1323.68236
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.