Scalable LCF-style proof translation

DOI10.1007/978-3-642-39634-2_7MaRDI QIDQ5327336zbMATH OpenOpenAlexWikidataFDO

Authors Cezary Kaliszyk, Alexander Krauss

Publication date 7 August 2013

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

Full work available at URL https://doi.org/10.1007/978-3-642-39634-2_7

Mathematics Subject Classification ID

Recommendations

• Importing HOL Light into Coq
• PRocH: proof reconstruction for HOL Light
• scientific article; zbMATH DE number 1670739
• A mechanized translation from higher-order logic to set theory
• An Interpretation of Isabelle/HOL in HOL Light

Cited in

(21)

• Aligning concepts across proof assistant libraries
• FoCaLiZe and Dedukti to the rescue for proof interoperability
• HOL(y)Hammer: online ATP service for HOL Light
• Experiences from exporting major proof assistant libraries
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Classification of alignments between concepts of formal mathematical systems
• From informal to formal proofs in Euclidean geometry
• Translating Scala programs to Isabelle/HOL. System description
• Learning-assisted theorem proving with millions of lemmas
• PRocH: proof reconstruction for HOL Light
• Proof auditing formalised mathematics
• A formal proof of the Kepler conjecture
• Matching concepts across HOL libraries
• Towards Knowledge Management for HOL Light
• A vernacular for coherent logic
• Fast LCF-Style Proof Reconstruction for Z3
• scientific article; zbMATH DE number 7649970 (Why is no real title available?)
• Formalising Mathematics in Simple Type Theory
• scientific article; zbMATH DE number 7756106 (Why is no real title available?)
• Translating HOL-Light proofs to Coq
• JEFL: joint embedding of formal proof libraries

Describes a project that uses

Uses Software

• Isabelle/HOL
• HOL Light

This page was built for publication: Scalable LCF-style proof translation

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