Importing HOL Light into Coq

DOI10.1007/978-3-642-14052-5_22zbMath1291.68353OpenAlexW1516654960MaRDI QIDQ5747657

Benjamin Werner, Chantal Keller

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

Related Items (18)

Classification of alignments between concepts of formal mathematical systems ⋮ JEFL: joint embedding of formal proof libraries ⋮ Aligning concepts across proof assistant libraries ⋮ FoCaLiZe and Dedukti to the rescue for proof interoperability ⋮ Making PVS accessible to generic services by interpretation in a universal format ⋮ Unnamed Item ⋮ Proof Assistants for Natural Language Semantics ⋮ The HOL Light theory of Euclidean space ⋮ Unnamed Item ⋮ A logical framework combining model and proof theory ⋮ A Foundational View on Integration Problems ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ Formalising foundations of mathematics ⋮ Experiences from exporting major proof assistant libraries ⋮ Matching Concepts across HOL Libraries ⋮ Towards Knowledge Management for HOL Light ⋮ A Vernacular for Coherent Logic ⋮ Proof Auditing Formalised Mathematics

Uses Software

• Coq
• HOL Light

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