nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Extensible and Efficient Automation Through Reflective Tactics

verfasst von : Gregory Malecha, Jesper Bengtson

Erschienen in: Programming Languages and Systems

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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}_{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}_{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}_{tac}\) through several case studies demonstrating orders of magnitude speedups for relatively little engineering work.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Probabilistic Functions and Cryptographic Oracles in Higher Order Logic

Nächstes Kapitel An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs

The full code can be found in the MirrorCore distribution.

We permit ill-typed terms in our representation to avoid indexing terms by their type. Indexed terms are larger which increases the time it takes to type-check them thus slowing down the automation.

In this definition we avoid the complexities of ill-typed terms. In the code, the soundness proof gets to assume that the context and goal are both well-typed.

Malecha’s work supports local quantification only in separation logic formulae and relies crucially on the type of separation logic formulae to be inhabited.

Agda Development Team. The Agda proof assistant reference manual, version 2.4.2. Accessed 2014 (2014)

Appel, A.W.: Program logics for certified compilers. Cambridge University Press, Cambridge (2014)CrossRefMATH

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)CrossRef

Barras, B., Werner, B.: Coq in Coq. Technical report, INRIA-Rocquencourt (1997)

Barzilay, E.: Implementing reflection in Nuprl. Ph.D. thesis, Cornell University, AAI3195788 (2005)

Barzilay, E., Allen, S., Constable, R.: Practical reflection in NuPRL. In: Short Paper Presented at LICS 2003, pp. 22–25, June 2003

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)CrossRef

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)CrossRef

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)CrossRef

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)CrossRef

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)CrossRef

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)CrossRef

13.

Chapman, J.: Type theory should eat itself. Electron. Notes Theoret. Comput. Sci. 228, 21–36 (2009)CrossRefMATH

14.

Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2008)MATH

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)

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)CrossRef

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)CrossRef

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)

21.

Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Proceedings of ICFP 2013, pp. 73–86. ACM (2013)

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)

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)CrossRef

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)

27.

Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings of ICFP 2002, pp. 235–246. ACM (2002)

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)CrossRef

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)CrossRef

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)

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)

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)

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)CrossRef

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)

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)CrossRef

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)CrossRef

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)

Titel: Extensible and Efficient Automation Through Reflective Tactics
verfasst von: Gregory Malecha
Jesper Bengtson
Verlag: Springer Berlin Heidelberg
Buch: Programming Languages and Systems
Print ISBN: 978-3-662-49497-4

Electronic ISBN: 978-3-662-49498-1

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-662-49498-1_21

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"