Steps towards Verified Implementations of HOL Light

DOI10.1007/978-3-642-39634-2_38MaRDI QIDQ5327372zbMATH OpenOpenAlexFDO

Authors Magnus O. Myreen, Scott Owens, Ramana Kumar

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_38

Mathematics Subject Classification ID

Recommendations

• Towards Self-verification of HOL Light
• Formalization of functional variation in HOL Light
• PRocH: proof reconstruction for HOL Light
• Enabling symbolic and numerical computations in HOL Light
• Proving Valid Quantified Boolean Formulas in HOL Light
• scientific article; zbMATH DE number 7594146

Cited in

(9)

• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Lemma Mining over HOL Light
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• HOL with definitions: semantics, soundness, and a verified implementation
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• scientific article; zbMATH DE number 2185701 (Why is no real title available?)
• Towards Self-verification of HOL Light
• Towards Knowledge Management for HOL Light
• Fast, verified computation for candle

Describes a project that uses

Uses Software

• HOL
• HOL Light
• Milawa
• Jitawa

This page was built for publication: Steps towards Verified Implementations of HOL Light

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