×

Extensible and efficient automation through reflective tactics. (English) Zbl 1335.68234

Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 532-559 (2016).
Summary: Foundational proof assistants simultaneously offer both expressive logics and strong guarantees. The price they pay for this flexibility is often the need to build and check explicit proof objects which can be expensive. In this work we develop a collection of techniques for building reflective automation, where proofs are witnessed by verified decision procedures rather than verbose proof objects. Our techniques center around a verified domain specific language for proving, \(\mathcal {R}_{\mathrm{tac}}\), written in Gallina, Coq’s logic. The design of tactics makes it easy to combine them into higher-level automation that can be proved sound in a mostly automated way. Furthermore, unlike traditional uses of reflection, \(\mathcal {R}_{\mathrm{tac}}\) tactics are independent of the underlying problem domain, which allows them to be re-tasked to automate new problems with very little effort. We demonstrate the usability of \(\mathcal {R}_{\mathrm{tac}}\) through several case studies demonstrating orders of magnitude speedups for relatively little engineering work.
For the entire collection see [Zbl 1333.68019].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Agda Development Team. The Agda proof assistant reference manual, version 2.4.2. Accessed 2014 (2014)
[2] Appel, A.W.: Program logics for certified compilers. Cambridge University Press, Cambridge (2014) · Zbl 1298.68009
[3] Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135–150. Springer, Heidelberg (2011) · Zbl 1350.68223
[4] Barras, B., Werner, B.: Coq in Coq. Technical report, INRIA-Rocquencourt (1997) · Zbl 1211.03023
[5] Barzilay, E.: Implementing reflection in Nuprl. Ph.D. thesis, Cornell University, AAI3195788 (2005)
[6] Barzilay, E., Allen, S., Constable, R.: Practical reflection in NuPRL. In: Short Paper Presented at LICS 2003, pp. 22–25, June 2003
[7] Bengtson, J., Jensen, J.B., Sieczkowski, F., Birkedal, L.: Verifying object-oriented programs with higher-order separation logic in Coq. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 22–38. Springer, Heidelberg (2011) · Zbl 1342.68203
[8] Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! a framework for higher-order separation logic in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 315–331. Springer, Heidelberg (2012) · Zbl 1360.68741
[9] Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2007) · Zbl 1178.03020
[10] Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular SMT proofs for fast reflexive checking inside Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 151–166. Springer, Heidelberg (2011) · Zbl 1350.68224
[11] Boespflug, M., Dénès, M., Grégoire, B.: Full reduction at full throttle. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 362–377. Springer, Heidelberg (2011) · Zbl 05977523
[12] Braibant, T., Pous, D.: Tactics for reasoning modulo AC in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 167–182. Springer, Heidelberg (2011) · Zbl 1350.68227
[13] Chapman, J.: Type theory should eat itself. Electron. Notes Theoret. Comput. Sci. 228, 21–36 (2009) · Zbl 1337.68057
[14] Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2008) · Zbl 1155.68429
[15] Chlipala, A.: From network interface to multithreaded web applications: a casestudy in modular program verification. In: Proceedings of POPL 2015, pp. 609–622. ACM (2015) · Zbl 06631333
[16] Claret, G., del Carmen González Huesca, L., Régis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 67–83. Springer, Heidelberg (2013) · Zbl 1317.68205
[17] Coq Development Team. The Coq proof assistant reference manual, version 8.4. Accessed 2012 (2015)
[18] Ricketts, D., Malecha, G., Alvarez, M.M., Gowda, V., Lerner, S.: Towards verification of hybrid systems in a foundational proof assistant. In: MEMOCODE 2015 (2015)
[19] Danielsson, N.A.: A formalisation of a dependently typed language as an inductive-recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 93–109. Springer, Heidelberg (2007) · Zbl 1178.03026
[20] Delaware, B., Pit-Claudel, C., Gross, J., Chlipala, A.: Fiat: deductive synthesis of abstract data types in a proof assistant. In: Proceedings of POPL 2015, pp. 689–700. ACM (2015) · Zbl 1346.68175
[21] Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Proceedings of ICFP 2013, pp. 73–86. ACM (2013) · Zbl 1323.68109
[22] Dodds, J., Cao, Q., Bengtson, J., Appel, A.W.: Computational symbolic execution in interactive Hoare-logic proofs (Under submission)
[23] Fallenstein, B., Kumar, R.: Proof-Producing Reflection for HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 170–186. Springer International Publishing, Switzerland (2015) · Zbl 1465.03052
[24] Garillot, F., Werner, B.: Simple types in type theory: deep and shallow encodings. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 368–382. Springer, Heidelberg (2007) · Zbl 1144.68355
[25] Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Rapport de recherche RR-6455, INRIA (2008)
[26] Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make Ad Hoc proof automation less Ad Hoc. In: Proceedings of ICFP 2011, pp. 163–175. ACM (2011) · Zbl 1323.68117
[27] Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings of ICFP 2002, pp. 235–246. ACM (2002) · Zbl 1322.68053
[28] Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307–322. Springer, Heidelberg (2010) · Zbl 1291.68353
[29] Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: Proceedings of SOSP, pp. 207–220. ACM (2009)
[30] Knoblock, T.B., Constable, R.L.: Formalized metareasoning in type theory. Technical report, Cornell University (1986)
[31] Kokke, P., Swierstra, W.: Auto in Agda. In: Hinze, R., Voigtländer, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 276–301. Springer, Heidelberg (2015) · Zbl 1432.68063
[32] Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd ACM symposium on Principles of Programming Languages, pp. 42–54. ACM Press (2006) · Zbl 1369.68124
[33] Lescuyer, S.: Formalisation et développement d’une tactique réflexive pourla démonstration automatique en Coq. Thèse de doctorat, Université Paris-Sud, January 2011
[34] Malecha, G., Chlipala, A., Braibant, T.: Compositional computational reflection. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 374–389. Springer, Heidelberg (2014) · Zbl 1416.68171
[35] Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: Proceedings of POPL 2010, pp. 237–248. ACM (2010) · Zbl 1312.68083
[36] Malecha, G., Wisnesky, R.: Using dependent types and tactics to enable semantic optimization of language-integrated queries. In: Proceedings of DBPL 2015, pp. 49–58. ACM (2015)
[37] Malecha, G.M.: Extensible proof engineering in intensional type theory. Ph.D. thesis, Harvard University, November 2014
[38] McBride, C.: Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In: Proceedings of WGP 2010, pp. 1–12. ACM (2010)
[39] Mike, S.: Homotopy type theory should eat itself (but so far, it’s too big to swallow), March 2014
[40] Pollack, R.: On extensibility of proof checkers. In: Smith, J., Dybjer, P., Nordström, B. (eds.) TYPES 1994. LNCS, vol. 996, pp. 140–161. Springer, Heidelberg (1995)
[41] Shao, Z.: Clean-slate development of certified OS kernels. In: Proceedings of CPP 2015, pp. 95–96. ACM (2015)
[42] Sozeau, M.: Proof-relevant rewriting strategies in Coq. In: At Coq Workshop, July 2014
[43] Stampoulis, A., Shao, Z.: VeriML: typed computation of logical terms inside a language with effects. In: Proceedings of ICFP, pp. 333–344. ACM (2010) · Zbl 1323.68384
[44] van der Walt, P., Swierstra, W.: Engineering proof by reflection in Agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157–173. Springer, Heidelberg (2013)
[45] Werner, B.: Sets in types, types in sets. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 530–546. Springer, Heidelberg (1997) · Zbl 0885.03017
[46] Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. In: Proceedings of ICFP 2013, pp. 87–100. ACM (2013) · 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.