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.

Two Applications of Logic Programming to Coq / M. Manighetti, D. Miller, A.D.A. Momigliano (LEIBNIZ INTERNATIONAL PROCEEDINGS IN INFORMATICS). - In: 26th International Conference on Types for Proofs and Programs (TYPES 2020) / [a cura di] U. de’Liguoro, S. Berardi, T. Altenkirch. - [s.l] : LIPICS, 2021. - ISBN 9783959771825. - pp. 10:1-10:19 (( Intervento presentato al 26. convegno TYPES tenutosi a Torino nel 2020 [10.4230/lipics.types.2020.10].

Two Applications of Logic Programming to Coq

A.D.A. Momigliano
2021

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.
Proof assistants; logic programming; Coq; λProlog; property-based testing
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
https://drops.dagstuhl.de/opus/volltexte/2021/13889/
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
LIPIcs-TYPES-2020-10.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 818.62 kB
Formato Adobe PDF
818.62 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/848817
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact