Steps towards Verified Implementations of HOL Light

DOI10.1007/978-3-642-39634-2_38zbMath1317.68225OpenAlexW1712305647MaRDI QIDQ5327372

Ramana Kumar, Magnus O. Myreen, Scott Owens

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

Related Items (2)

The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation

Uses Software

• HOL
• HOL Light
• Milawa
• Jitawa

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