Importing HOL Light into Coq

DOI10.1007/978-3-642-14052-5_22MaRDI QIDQ5747657zbMATH OpenOpenAlexFDO

Authors Chantal Keller, Benjamin Werner

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14052-5_22

Mathematics Subject Classification ID

Recommendations

• HOCore in Coq
• An Isabelle-like procedural mode for HOL Light
• scientific article; zbMATH DE number 1670739
• Interfacing Coq + SSReflect with GAP
• Towards Rewriting in Coq
• Formalization of Habanero phasers using Coq
• A Sound Semantics for OCaml light
• Implementing hash-consed structures in Coq

Cited in

(23)

• A logical framework combining model and proof theory
• JEFL: joint embedding of formal proof libraries
• Changing data representation within the \textsf{Coq} system
• Importing mathematics from HOL into Nuprl
• Towards Knowledge Management for HOL Light
• scientific article; zbMATH DE number 7649970 (Why is no real title available?)
• Aligning concepts across proof assistant libraries
• Matching concepts across HOL libraries
• Proof assistants for natural language semantics
• A foundational view on integration problems
• Conversion of HOL Light proofs into Metamath
• Classification of alignments between concepts of formal mathematical systems
• scientific article; zbMATH DE number 7756106 (Why is no real title available?)
• An Interpretation of Isabelle/HOL in HOL Light
• Formalising foundations of mathematics
• Experiences from exporting major proof assistant libraries
• Making PVS accessible to generic services by interpretation in a universal format
• The HOL Light theory of Euclidean space
• FoCaLiZe and Dedukti to the rescue for proof interoperability
• Extensible and efficient automation through reflective tactics
• Proof auditing formalised mathematics
• A vernacular for coherent logic
• Scalable LCF-style proof translation

Describes a project that uses

Uses Software

• HOL Light
• Coq

This page was built for publication: Importing HOL Light into Coq

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