Document Open Access Logo

Two Applications of Logic Programming to Coq

Authors Matteo Manighetti, Dale Miller, Alberto Momigliano

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.10.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Author Details

Matteo Manighetti
  • Inria, Palaiseau, France
  • LIX, Ecole Polytechnique, Palaiseau, France
Dale Miller
  • Inria, Palaiseau, France
  • LIX, Ecole Polytechnique, Palaiseau, France
Alberto Momigliano
  • Dipartimento di Informatica, University of Milan, Italy

Acknowledgements

We thank Enrico Tassi for his help with Coq-Elpi. His comments and those of the anonymous reviewers on an early draft of this paper have also been very helpful.

Cite AsGet BibTex

Matteo Manighetti, Dale Miller, and Alberto Momigliano. Two Applications of Logic Programming to Coq. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TYPES.2020.10

Abstract

The logic programming paradigm provides a flexible setting for representing, manipulating, checking, and elaborating proof structures. This is particularly true when the logic programming language allows for bindings in terms and proofs. In this paper, we make use of two recent innovations at the intersection of logic programming and proof checking. One of these is the foundational proof certificate (FPC) framework which provides a flexible means of defining the semantics of a range of proof structures for classical and intuitionistic logic. A second innovation is the recently released Coq-Elpi plugin for Coq in which the Elpi implementation of λProlog can send and retrieve information to and from the Coq kernel. We illustrate the use of both this Coq plugin and FPCs with two example applications. First, we implement an FPC-driven sequent calculus for a fragment of the Calculus of Inductive Constructions and we package it into a tactic to perform property-based testing of inductive types corresponding to Horn clauses. Second, we implement in Elpi a proof checker for first-order intuitionistic logic and demonstrate how proof certificates can be supplied by external (to Coq) provers and then elaborated into the fully detailed proof terms that can be checked by the Coq kernel.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Proof assistants
  • logic programming
  • Coq
  • λProlog
  • property-based testing

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. of Logic and Computation, 2(3):297-347, 1992. URL: https://doi.org/10.1093/logcom/2.3.297.
  2. David Baelde. Least and greatest fixed points in linear logic. ACM Trans. on Computational Logic, 13(1):2:1-2:44, 2012. URL: https://doi.org/10.1145/2071368.2071370.
  3. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. Journal of Formalized Reasoning, 7(2):1-89, 2014. URL: https://doi.org/10.6092/issn.1972-5787/4650.
  4. Nick Benton, Chung-Kil Hur, Andrew Kennedy, and Conor McBride. Strongly typed term representations in Coq. J. Autom. Reason., 49(2):141-159, 2012. URL: https://doi.org/10.1007/s10817-011-9219-0.
  5. G. Bierman. On Intuitionistic Linear Logic. PhD thesis, Computing Laboratory, University of Cambridge, 1994. Google Scholar
  6. Roberto Blanco, Zakaria Chihani, and Dale Miller. Translating between implicit and explicit versions of proof. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 255-273. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_16.
  7. Roberto Blanco, Matteo Manighetti, and Dale Miller. FPC-Coq: Using Elpi to elaborate external proof evidence into Coq proofs. Technical Report hal-02974002, Inria, July 2020. Presented at the Coq Workshop 2020. URL: https://hal.inria.fr/hal-02974002.
  8. Roberto Blanco and Dale Miller. Proof outlines as proof certificates: a system description. In Iliano Cervesato and Carsten Schürmann, editors, Proceedings First International Workshop on Focusing, volume 197 of Electronic Proceedings in Theoretical Computer Science, pages 7-14. Open Publishing Association, 2015. URL: https://doi.org/10.4204/EPTCS.197.2.
  9. Roberto Blanco, Dale Miller, and Alberto Momigliano. Property-based testing via proof reconstruction. In E. Komendantskaya, editor, Principles and Practice of Programming Languages 2019 (PPDP '19), October 2019. URL: https://doi.org/10.1145/3354166.3354170.
  10. Matteo Cavada, Andrea Colò, and Alberto Momigliano. MutantChick: Type-preserving mutation analysis for Coq. In CILC, volume 2710 of CEUR Workshop Proceedings, pages 105-112. CEUR-WS.org, 2020. URL: http://ceur-ws.org/Vol-2710/short2.pdf.
  11. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Journal of Logic and Computation, 13(5):639-688, 2003. URL: https://doi.org/10.1093/logcom/13.5.639.
  12. Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A multi-focused proof system isomorphic to expansion proofs. J. of Logic and Computation, 26(2):577-603, 2016. URL: https://doi.org/10.1093/logcom/exu030.
  13. Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In G. Ausiello, J. Karhumäki, G. Mauri, and L. Ong, editors, Fifth International Conference on Theoretical Computer Science, volume 273 of IFIP, pages 383-396. Springer, September 2008. URL: https://doi.org/10.1007/978-0-387-09680-3_26.
  14. James Cheney and Alberto Momigliano. αCheck: A mechanized metatheory model checker. Theory and Practice of Logic Programming, 17(3):311–352, 2017. URL: https://doi.org/10.1017/S1471068417000035.
  15. James Cheney, Alberto Momigliano, and Matteo Pessina. Advances in property-based testing for backslashalpha prolog. In TAP@STAF, volume 9762 of Lecture Notes in Computer Science, pages 37-56. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41135-4_3.
  16. Zakaria Chihani, Dale Miller, and Fabien Renaud. A semantic framework for proof evidence. J. of Automated Reasoning, 59(3):287-330, 2017. URL: https://doi.org/10.1007/s10817-016-9380-6.
  17. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In James Hook and Peter Thiemann, editors, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pages 143-156. ACM, 2008. URL: https://doi.org/10.1145/1411204.1411226.
  18. Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy builder: Algebraic hierarchies made easy in coq with elpi (system description). In FSCD, volume 167 of LIPIcs, pages 34:1-34:21. Schloss Dagstuhl, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.34.
  19. Joëlle Despeyroux, Amy Felty, and Andre Hirschowitz. Higher-order abstract syntax in Coq. In Second International Conference on Typed Lambda Calculi and Applications, pages 124-138. Springer, April 1995. URL: https://doi.org/10.1007/BFb0014049.
  20. Cvetan Dunchev, Claudio Sacerdoti Coen, and Enrico Tassi. Implementing HOL in an higher order logic programming language. In LFMTP, pages 4:1-4:10. ACM, 2016. URL: https://doi.org/10.1145/2966268.2966272.
  21. Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. ELPI: fast, embeddable, λprolog interpreter. In LPAR, volume 9450 of Lecture Notes in Computer Science, pages 460-468. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_32.
  22. Amy Felty. Encoding the calculus of constructions in a higher-order logic. In M. Vardi, editor, 8th Symp. on Logic in Computer Science, pages 233-244. IEEE, June 1993. URL: https://doi.org/10.1109/LICS.1993.287584.
  23. Amy Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43-81, 1993. URL: https://doi.org/10.1007/BF00881900.
  24. Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In Ninth International Conference on Automated Deduction, number 310 in Lecture Notes in Computer Science, pages 61-80, Argonne, IL, 1988. Springer. URL: https://doi.org/10.1007/BFb0012823.
  25. Burke Fetscher, Koen Claessen, Michal H. Palka, John Hughes, and Robert Bruce Findler. Making random judgments: Automatically generating well-typed terms from the definition of a type-system. In ESOP, volume 9032 of Lecture Notes in Computer Science, pages 383-405. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_16.
  26. George Fink and Matt Bishop. Property-based testing: a new approach to testing for assurance. ACM SIGSOFT Software Engineering Notes, pages 74-80, July 1997. URL: https://doi.org/10.1145/263244.263267.
  27. Fabio Fioravanti, Maurizio Proietti, and Valerio Senni. Efficient generation of test data structures using constraint logic programming and program transformation. J. Log. Comput., 25(6):1263-1283, 2015. URL: https://doi.org/10.1093/logcom/ext071.
  28. Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. J. of Automated Reasoning, 49(2):241-273, 2012. URL: https://doi.org/10.1007/s10817-011-9218-1.
  29. Gerhard Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68-131. North-Holland, Amsterdam, 1935. URL: https://doi.org/10.1007/BF01201353.
  30. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  31. Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer, 1979. URL: https://doi.org/10.1007/3-540-09724-4.
  32. Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. Implementing type theory in higher order constraint logic programming. Mathematical Structures in Computer Science, 29(8):1125-1150, 2019. URL: https://doi.org/10.1017/S0960129518000427.
  33. John Hannan. Extended natural semantics. J. of Functional Programming, 3(2):123-152, April 1993. URL: https://doi.org/10.1017/S0956796800000666.
  34. Hugo Herbelin. A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure. In CSL, volume 933 of Lecture Notes in Computer Science, pages 61-75. Springer, 1994. URL: https://doi.org/10.1007/BFb0022247.
  35. Furio Honsell, Marino Miculan, and Ivan Scagnetto. π-calculus in (co)inductive type theories. Theoretical Computer Science, 2(253):239-285, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00095-5.
  36. Martin Hyland and Valeria de Paiva. Full intuitionistic linear logic (extended abstract). Annals of Pure and Applied Logic, 64(3):273-291, 11 November 1993. URL: https://doi.org/10.1016/0168-0072(93)90146-5.
  37. Gilles Kahn. Natural semantics. In Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing, editors, Proceedings of the Symposium on Theoretical Aspects of Computer Science, volume 247 of Lecture Notes in Computer Science, pages 22-39. Springer, 1987. URL: https://doi.org/10.1007/BFb0039592.
  38. Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. Run your research: on the effectiveness of lightweight mechanization. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '12, pages 285-296, New York, NY, USA, 2012. ACM. URL: https://doi.org/10.1145/2103656.2103691.
  39. Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. Generating good generators for inductive relations. Proc. ACM Program. Lang., 2(POPL):45:1-45:30, 2018. URL: https://doi.org/10.1145/3158133.
  40. Stéphane Lengrand. Normalisation & Equivalence in Proof Theory & Type Theory. PhD thesis, University of St. Andrews, December 2006. URL: https://tel.archives-ouvertes.fr/tel-00134646.
  41. Stéphane Lengrand, Roy Dyckhoff, and James McKinna. A sequent calculus for type theory. In CSL, volume 4207 of Lecture Notes in Computer Science, pages 441-455. Springer, 2006. URL: https://doi.org/10.1007/11874683_29.
  42. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, 2009. URL: https://doi.org/10.1016/j.tcs.2009.07.041.
  43. J.W. Lloyd and J.C. Shepherdson. Partial evaluation in logic programming. The Journal of Logic Programming, 11(3):217-242, 1991. URL: https://doi.org/10.1016/0743-1066(91)90027-M.
  44. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1(4):497-536, 1991. URL: https://doi.org/10.1093/logcom/1.4.497.
  45. Dale Miller. Proof checking and logic programming. Formal Aspects of Computing, 29(3):383-399, 2017. URL: https://doi.org/10.1007/s00165-016-0393-z.
  46. Dale Miller. Mechanized metatheory revisited. Journal of Automated Reasoning, 63(3):625-665, October 2019. URL: https://doi.org/10.1007/s10817-018-9483-3.
  47. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, 2012. URL: https://doi.org/10.1017/CBO9781139021326.
  48. Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125-157, 1991. URL: https://doi.org/10.1016/0168-0072(91)90068-W.
  49. Robin Milner. Communication and Concurrency. Prentice-Hall International, 1989. Google Scholar
  50. Gopalan Nadathur and Dale Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777-814, 1990. URL: https://doi.org/10.1145/96559.96570.
  51. Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus - A compiler and abstract machine based implementation of λProlog. In H. Ganzinger, editor, 16th Conf. on Automated Deduction (CADE), number 1632 in LNAI, pages 287-291, Trento, 1999. Springer. URL: https://doi.org/10.1007/3-540-48660-7_25.
  52. Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational property-based testing. In Christian Urban and Xingyuan Zhang, editors, ITP 2015, volume 9236 of Lecture Notes in Computer Science, pages 325-343. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_22.
  53. Lawrence C. Paulson. The foundation of a generic theorem prover. J. Autom. Reason., 5(3):363-397, 1989. URL: https://doi.org/10.1007/BF00248324.
  54. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199-208. ACM Press, June 1988. URL: https://doi.org/10.1145/53990.54010.
  55. Brigitte Pientka and Joshua Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In J. Giesl and R. Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, number 6173 in Lecture Notes in Computer Science, pages 15-21, 2010. URL: https://doi.org/10.1007/978-3-642-14203-1_2.
  56. Elaine Pimentel, Vivek Nigam, and Jo ao Neto. Multi-focused proofs with different polarity assignments. In Mario Benevides and Rene Thiemann, editors, Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015), volume 323 of Electronic Notes in Theoretical Computer Science, pages 163-179, 2016. URL: https://doi.org/10.1016/j.entcs.2016.06.011.
  57. Gordon D. Plotkin. A structural approach to operational semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark, 1981. Google Scholar
  58. Thomas Raths, Jens Otten, and Christoph Kreitz. The ILTP problem library for intuitionistic logic. Journal of Automated Reasoning, 38(1):261-271, 2007. URL: https://doi.org/10.1007/s10817-006-9060-z.
  59. C. Röckl, D. Hirschkoff, and S. Berghofer. Higher-order abstract syntax with induction in Isabelle/HOL: Formalizing the pi-calculus and mechanizing the theory of contexts. In F. Honsell and M. Miculan, editors, Proc. FOSSACS'01, volume 2030 of Lecture Notes in Computer Science, pages 364-378. Springer, 2001. URL: https://doi.org/10.1007/3-540-45315-6_24.
  60. Colin Runciman, Matthew Naylor, and Fredrik Lindblad. Smallcheck and Lazy Smallcheck: automatic exhaustive testing for small values. In Andy Gill, editor, Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, Haskell 2008, Victoria, BC, Canada, 25 September 2008, pages 37-48. ACM, 2008. URL: https://doi.org/10.1145/1411286.1411292.
  61. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The metacoq project. J. Autom. Reason., 64(5):947-999, 2020. URL: https://doi.org/10.1007/s10817-019-09540-0.
  62. Enrico Tassi. Elpi: an extension language for Coq. CoqPL 2018: The Fourth International Workshop on Coq for Programming Languages, 2018. URL: https://hal.inria.fr/hal-01637063/.
  63. Enrico Tassi. Deriving proved equality tests in Coq-Elpi: Stronger induction principles for containers in Coq. In ITP, volume 141 of LIPIcs, pages 29:1-29:18. Schloss Dagstuhl, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.29.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact