Candle: a verified implementation of HOL Light (extended version)
From MaRDI portal
Cites work
- A Brief Overview of HOL4
- A mechanised semantics for HOL with ad-hoc overloading
- A verified cyclicity checker: for theories with overloaded constants
- A verified runtime for a verified theorem prover
- Candle: a verified implementation of HOL light
- Fast, verified computation for HOL ITPs
- From LCF to Isabelle/HOL
- HOL Zero's solutions for Pollack-inconsistency
- Isabelle's metalogic: formalization and proof checker
- Mechanisation of model-theoretic conservative extension for HOL with ad-hoc overloading
- Metamath Zero: designing a theorem prover prover
- Proof-producing synthesis of CakeML from monadic HOL functions
- Proof-producing translation of higher-order logic into pure and stateful ML
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Sets in Coq, Coq in Sets
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- The verified CakeML compiler backend
- Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
- Towards a formally verified proof assistant
- Towards Self-verification of HOL Light
This page was built for publication: Candle: a verified implementation of HOL Light (extended version)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6862767)
