Candle: a verified implementation of HOL Light (extended version)

DOI10.1007/S10817-025-09743-8MaRDI QIDQ6862767zbMATH OpenFDO

Authors Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas D. Sewell

Publication date 6 February 2026

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

higher-order logicinteractive theorem provingprover soundness

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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)