Skip to Main content Skip to Navigation
Reports

FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs

Roberto Blanco 1 Matteo Manighetti 2 Dale Miller 2
2 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Logic programming implementations of the foundational proof certificate(FPC) framework are capable of checking a wide range of proof evidence. Proof checkers based on logic programming can make use of both unification and backtracking search to allow varying degrees of proof reconstructionto take place during proof checking. Such proof checkers are also able to elaborate proofs lacking full details into proofs containing much more detail. We outline here our use of the Coq-Elpi plugin, which embeds an implementation of λProlog into Coq, to check proof certificates supplied by external (toCoq) provers and to elaborate them into the fully detailed proof terms that are needed for checkingby the Coq kernel.
Document type :
Reports
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-02974002
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Wednesday, October 21, 2020 - 2:50:31 PM
Last modification on : Saturday, May 1, 2021 - 3:39:18 AM
Long-term archiving on: : Friday, January 22, 2021 - 6:47:35 PM

File

fpccoq-draft.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02974002, version 1

Citation

Roberto Blanco, Matteo Manighetti, Dale Miller. FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs. [Research Report] Inria Saclay. 2020. ⟨hal-02974002⟩

Share

Metrics

Record views

82

Files downloads

142