Candle: a verified implementation of HOL light

DOI10.4230/LIPICS.ITP.2022.3MaRDI QIDQ6572534zbMATH OpenFDO

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

Publication date 15 July 2024

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2022.3

zbMATH Keywords

higher-order logicinteractive theorem provingprover soundness

Mathematics Subject Classification ID

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

Cited in

(7)

• Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
• Mechanized HOL reasoning in set theory
• Candle: a verified implementation of HOL Light (extended version)
• Faithful logic embeddings in HOL -- deep and shallow
• Fast, verified computation for HOL ITPs
• Accelerating and verifying constant-time modular inversion
• Understanding binary-Goppa decoding

This page was built for publication: Candle: a verified implementation of HOL light

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6572534)