Recycling Proof Patterns in Coq: Case Studies

1. Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: An approach. Kluwer Academic Publishers, Norwell (2000)

2. Bove, A., et al.: (2009) A brief overview of agda—a functional language with dependent types. In: 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs’09) LNCS, vol. 5674, pp. 73–78 (2009)

3. Coq development team. The Coq Proof Assistant Reference Manual, version 8.4. Technical report (2012)

4. Nipkow, T., et al.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283, Springer, Berlin (2002)

5. Asperti, A., et al.: The Matita interactive theorem prover. In: 23rd International Conference on Automated Deduction (CADE’11), LNCS, vol. 6803, pp. 64–69 (2011)

6. Grabowski A., Kornilowicz A., Naumowicz A.: Mizar in a nutshell. J. Formaliz. Reason. 3(2), 153–245 (2010)

   MATH  MathSciNet  Google Scholar 

7. Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: 4th Conference on Interactive Theorem Proving (ITP’13), LNCS, vol. 7998, pp. 163–179 (2013)

8. Krebbers R., Spitters B.: Type classes for efficient exact real arithmetic in Coq. Log. Methods Comput. Sci. 9(1), 1–27 (2013)

   Article  MathSciNet  Google Scholar 

9. Hales, T.: The Flyspeck Project fact sheet. Project description. Available at http://code.google.com/p/flyspeck/ (2005)

10. Amorim, A., et al.: A verified information-flow architecture. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14) (2014)

11. Benton, N.: Machine Obstructed Proof: How many months can it take to verify 30 assembly instructions? (2006)

12. Heras, J., Komendantskaya, E.: ML4PG: downloadable programs, manual, examples (2012–2014). http://staff.computing.dundee.ac.uk/katya/ML4PG/

13. Heras, J., Komendantskaya, E.: Proof Pattern Search in Coq/SSReflect (2014) http://arxiv.org/abs/1402.0081

14. Komendantskaya E. et al.: Machine learning for proof general: interfacing interfaces. Electron. Proc. Theor. Comput. Sci. 118, 15–41 (2013)

    Article  Google Scholar 

15. Aspinall, D.: Proof General: A generic tool for proof development. In: 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00), LNCS, vol. 1785, pp. 38–43 (2000)

16. Bertot Y., Castéran P.: Interactive Theorem Proving and Program Development, Coq’Art: the Calculus of Constructions. Springer, Berlin (2004)

    Book  Google Scholar 

17. Gonthier G., Mahboubi A.: An introduction to small scale reflection. J. Formaliz. Reason. 3(2), 95–152 (2010)

    MATH  MathSciNet  Google Scholar 

18. Gonthier G.: Formal proof—the four-color theorem. Notices Am. Math. Soc. 55(11), 1382–1393 (2008)

    MATH  MathSciNet  Google Scholar 

19. Le Roux, S.: Acyclic preferences and existence of sequential nash equilibria: a formal and constructive equivalence. In: 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’07), LNCS, vol. 5674, pp. 293–309 (2009)

20. Vestergaard R.: A constructive approach to sequential nash equilibria. Inf. Process. Lett. 97, 46–51 (2006)

    Article  MATH  MathSciNet  Google Scholar 

21. Moore, J S.: Models, Algebras and Logic of Engineering Software. In: Proving Theorems about Java and the JVM with ACL2, pp. 227–290. IOS Press, Amsterdam (2004)

22. Bundy A. et al.: AI meets Formal Software Development (Dagstuhl Seminar 12271). Dagstuhl Rep. 2(7), 1–29 (2012)

    Google Scholar 

23. Johansson M. et al.: Conjecture synthesis for inductive theories. J. Autom. Reason. 47(3), 251–289 (2011)

    Article  MATH  MathSciNet  Google Scholar 

24. Basin D. et al.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge (2005)

    Google Scholar 

25. Kühlwein, D., et al.:Overview and evaluation of premise selection techniques for large theory mathematics. In: 6th International Joint Conference on Automated Reasoning (IJCAR’12), LNCS, vol. 7364, pp. 378–392 (2012)

26. Duncan, H.: The use of Data-Mining for the Automatic Formation of Tactics. PhD thesis, University of Edinburgh (2002)

27. Asperti, A., et al.: A content based mathematical search engine: Whelp. In: Post-Proceedings of the TYPES’04 International Conference, LNCS, vol. 3839, pp. 17–32 (2006)

28. Bishop C.: Pattern Recognition and Machine Learning. Springer, Berlin (2006)

    MATH  Google Scholar 

29. Blum A.: Learning boolean functions in an infinite attribute space. Mach. Learn. 9(4), 373–386 (1992)

    MATH  Google Scholar 

30. MATLAB.: version 7.14.0 (R2012a). The MathWorks Inc., Natick, Massachusetts (2012)

31. Hall M. et al.: The WEKA data mining software: an update. SIGKDD Explor. 11(1), 10–18 (2009)

    Article  Google Scholar 

32. Heras, J., et al.: roof-pattern recognition and lemma discovery in ACL2. In: 19th Logic for Programming Artificial Intelligence and Reasoning (LPAR-19), LNCS, vol. 8312, pp. 389–406 (2013)

33. Le Roux, S.: Acyclicity and finite linear extendability: a formal and constructive equivalence. In: 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs’09), Emerging Trends Proceedings, pp. 154–169 (2007)

34. Lindholm, T., et al.: The Java Virtual Machine Specification: Java SE 7 edn. (2012)

35. Lange, C., et al.: A qualitative comparison of the suitability of four theorem provers for basic auction theory. In: Proceedings of Conferences on Intelligent Computer Mathematics (CICM’13), LNCS, vol. 7961, pp. 200–215 (2012)

Download references