Steps towards Verified Implementations of HOL Light
From MaRDI portal
Publication:5327372
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
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
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)