Translating HOL-Light proofs to Coq

DOI10.29007/6K4XMaRDI QIDQ7025200zbMATH OpenFDO

Authors Frédéric Blanqui

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/6K4X

zbMATH Keywords

rewritinghigher-order logiclogical frameworksdependent type theoryproof translationproof transformationconcept alignment

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 1670739 (Why is no real title available?)
• scientific article; zbMATH DE number 1863394 (Why is no real title available?)
• scientific article; zbMATH DE number 7649970 (Why is no real title available?)
• A formal proof of the Kepler conjecture
• A formulation of the simple theory of types.
• A framework for defining logics
• A modular construction of type theories
• An introduction to mathematical logic and type theory: To truth through proof.
• Canonical structures for the working Coq user
• Conversion of HOL Light proofs into Metamath
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• HOL Light: An Overview
• Importing HOL Light into Coq
• Importing mathematics from HOL into Nuprl
• Logic and Computation
• Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
• Scalable LCF-style proof translation
• Sharing a library between proof assistants: reaching out to the HOL family
• The new rewriting engine of dedukti (system description)

Cited in

(3)

• Checking linear integer arithmetic proofs in Lambdapi
• Indexing and retrieval in a heterogeneous formal library
• Interoperability of proof systems with SC-TPTP

This page was built for publication: Translating HOL-Light proofs to Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7025200)