Hostname: page-component-8448b6f56d-xtgtn Total loading time: 0 Render date: 2024-04-24T00:40:18.346Z Has data issue: false hasContentIssue false
  • English
  • Français

How to make ad hoc proof automation less ad hoc

Part of: JFP Research Articles

Published online by Cambridge University Press:  29 October 2013

GEORGES GONTHIER ,
BETA ZILIANI ,
ALEKSANDAR NANEVSKI  and
DEREK DREYER
GEORGES GONTHIER
Affiliation:
Microsoft Research, Cambridge, United Kingdom (e-mail: gonthier@microsoft.com)
BETA ZILIANI
Affiliation:
Max Planck Institute for Software Systems (MPI-SWS), Saarbrücken, Germany (e-mail: beta@mpi-sws.org)
ALEKSANDAR NANEVSKI
Affiliation:
IMDEA Software Institute, Madrid, Spain (e-mail: aleks.nanevski@imdea.org)
DEREK DREYER
Affiliation:
Max Planck Institute for Software Systems (MPI-SWS), Saarbrücken, Germany (e-mail: dreyer@mpi-sws.org)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself.

We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.

Type
Articles
Information
Journal of Functional Programming , Volume 23 , Issue 4: ICFP 2011 , July 2013 , pp. 357 - 401
Copyright
Copyright © Cambridge University Press 2013 

References

Asperti, A., Ricciotti, W., Coen, C. S. & Tassi, E. (2009) Hints in unification. In Theorem Proving in Higher Order Logics, LNCS, Vol. 5674. Springer, pp. 84–98.CrossRefGoogle Scholar
Barras, B., Jouannaud, J.-P., Strub, P.-Y. & Wang, Q. (2011) CoqMTU: A higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory. In Twenty-Sixth Annual IEEE Symposium on Logic in Computer Science. IEEE, pp. 143–151.Google Scholar
Bertot, Y., Gonthier, G., Ould Biha, S. & Pasca, I. (2008) Canonical big operators. In TPHOLs, LNCS, Vol. 5170. Springer, pp. 86–101.Google Scholar
Braibant, T. & Pous, D. (2010) Rewriting modulo associativity and commutativity in Coq. Second Coq Workshop.Google Scholar
Chakravarty, M. M. T., Keller, G. & Peyton Jones, S. (2005) Associated type synonyms. In ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 241–253.Google Scholar
Chlipala, A. (2008) Certified Programming with Dependent Types. Available at: http://adam.hlipala.net/cpdt.Google Scholar
Chlipala, A. (2011) Mostly-automated verification of low-level programs in computational separation logic. In Proceedings of the ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation. ACM, pp. 234–245.Google Scholar
Goldfarb, W. D. (1981) The undecidability of the second-order unification problem. Theor. Comput. Sci. 13 (2), 225–230.CrossRefGoogle Scholar
Gonthier, G. (2008) Formal proof – the four-color theorem. Not. AMS 55 (11), 1382–1393.Google Scholar
Gonthier, G. (2011) Point-free, set-free concrete linear algebra. In Interactive Theorem Proving, LNCS, Vol. 6898. Springer, pp 103–118.CrossRefGoogle Scholar
Gonthier, G. & Mahboubi, A. (2010) An introduction to small scale reflection in Coq. J. Formalized Reason. 3 (2), 95–152.Google Scholar
Gonthier, G., Ziliani, B., Nanevski, A. & Dreyer, D. (2012) How to make ad hoc proof automation less ad hoc. Supporting material available at: http://www.mpi-sws.org/~beta/lessadhoc.CrossRefGoogle Scholar
Grégoire, B. & Mahboubi, A. (2005) Proving equalities in a commutative ring done right in Coq. In Theorem Proving in Higher Order Logics, LNCS, Vol. 3603. Springer, pp. 98–113.CrossRefGoogle Scholar
Hall, C., Hammond, K., Jones, S. P. & Wadler, P. (1996) Type classes in Haskell. ACM Trans. Program. Lang. Syst. 18 (2), 241–256.CrossRefGoogle Scholar
Jia, L., Zhao, J., Sjöberg, V. & Weirich, S. (2010) Dependent types and program equivalence. In Proceedings of the ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages. ACM, pp. 275–286.Google Scholar
Jones, M. P. (2000) Type classes with functional dependencies. In Proceedings of the European Symposium on Programming, LNCS, Vol. 1782. Springer, pp. 230–244.Google Scholar
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 53 (6), 107–115.CrossRefGoogle Scholar
Leroy, X. (2009) Formal verification of a realistic compiler. Commun. ACM 52 (7), 107–115.CrossRefGoogle Scholar
Miller, D. (1991) Unification of simply typed lambda-terms as logic programming. In International Conference on Logic Programming, Seattle, WA, USA, MIT Press, pp. 255–269.Google Scholar
Morris, J. G. & Jones, M. P. (2010) Instance chains: type class programming without overlapping instances. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 375–386.CrossRefGoogle Scholar
Nanevski, A., Vafeiadis, V. & Berdine, J. (2010) Structuring the verification of heap-manipulating programs. In Proceedings of the 37th annual ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages. ACM, pp. 261–274.Google Scholar
Pientka, B. & Dunfield, J. (2008) Programming with proofs and explicit contexts. In ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. ACM, pp. 163–173.Google Scholar
Poswolsky, A. & Schürmann, C. (2009) System description: Delphin – a functional programming language for deductive systems. Electron. Notes Theor. Comput. Sci. 228, 113–120.CrossRefGoogle Scholar
Reynolds, J. C. (2002) Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. IEEE, pp. 55–74.Google Scholar
Saïbi, A. (1997) Typing algorithm in type theory with inheritance. In Proceedings of the 24th ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages. ACM, pp. 292–301.CrossRefGoogle Scholar
Sozeau, M. & Oury, N. (2008) First-class type classes. In Theorem Proving in Higher Order Logics, LNCS, Vol. 5170. Springer, pp. 278–293.CrossRefGoogle Scholar
Spitters, B. & van der Weegen, E. (2011) Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21 (4), 795–825.Google Scholar
Stampoulis, A. & Shao, Z. (2010) VeriML: Typed computation of logical terms inside a language with effects. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 333–344.CrossRefGoogle Scholar
Stampoulis, A. & Shao, Z. (2012) Static and user-extensible proof checking. In 39th ACM Symposium on Principles of Programming Languages. ACM, pp. 273–284.Google Scholar
Strub, P.-Y. (2010) Coq modulo theory. In Computer Science Logic, LNCS, Vol. 6247. Springer, pp. 529–543.CrossRefGoogle Scholar
Wadler, P. & Blott, S. (1989) How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th Annual ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages. ACM, pp. 60–76.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.