Fast, verified computation for candle

DOI10.4230/LIPICS.ITP.2023.4MaRDI QIDQ6642975zbMATH OpenFDO

Authors Oskar Abrahamsson, Magnus O. Myreen

Publication date 26 November 2024

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

zbMATH Keywords

higher-order logicinteractive theorem provingprover soundness

Mathematics Subject Classification ID

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

Recommendations

• Verified interactive computation of definite integrals
• Steps towards Verified Implementations of HOL Light
• scientific article; zbMATH DE number 1670747
• CakeML

Cited in

(2)

• Fast, verified computation for HOL ITPs
• Soundness of the Q0 proof system for higher-order logic

This page was built for publication: Fast, verified computation for candle

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