Steps towards Verified Implementations of HOL Light

DOI10.1007/978-3-642-39634-2_38zbMATH Open1317.68225OpenAlexW1712305647MaRDI QIDQ5327372FDOQ5327372

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

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

Mathematics Subject Classification ID

Cited In (9)

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

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)