Importing HOL Light into Coq
From MaRDI portal
Publication:5747657
DOI10.1007/978-3-642-14052-5_22zbMATH Open1291.68353OpenAlexW1516654960MaRDI QIDQ5747657FDOQ5747657
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
Recommendations
Cited In (23)
- A logical framework combining model and proof theory
- Changing data representation within the \textsf{Coq} system
- JEFL: joint embedding of formal proof libraries
- Importing mathematics from HOL into Nuprl
- Towards Knowledge Management for HOL Light
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- Classification of alignments between concepts of formal mathematical systems
- 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
- A vernacular for coherent logic
- Proof auditing formalised mathematics
- Extensible and efficient automation through reflective tactics
- Scalable LCF-style proof translation
Uses Software
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)
