Asset Details
Do you wish to reserve the book?
Fast, Verified Computation for HOL ITPs
Hey, we have placed the reservation for you!
By the way, why not check out events that you can attend while you pick your title.
Oops! Something went wrong.
Looks like we were not able to place the reservation. Kindly try again later.
Are you sure you want to remove the book from the shelf?
Fast, Verified Computation for HOL ITPs
Do you wish to request the book?
Fast, Verified Computation for HOL ITPs
Please be aware that the book you have requested cannot be checked out. If you would like to checkout this book, you can reserve another copy
We have requested the book for you!
Your request is successful and it will be processed during the Library working hours. Please check the status of your request in My Requests.
Oops! Something went wrong.
Looks like we were not able to place your request. Kindly try again later.
Journal Article
Fast, Verified Computation for HOL ITPs
2025
Overview
We add an efficient function for computation to the kernels of higher-order logic interactive theorem provers. First, we develop and prove sound our approach for Candle. Candle is a port of HOL Light which has been proved sound with respect to the inference rules of its higher-order logic; we extend its implementation and soundness proof. Second, we replicate our now-verified implementation for HOL4 with only minor changes, and build additional automation for ease of use. The automation exists outside of the HOL4 kernel, and requires no additional trust. We exercise our new computation function and associated automation on the evaluation of the CakeML compiler backend within HOL4’s logic, demonstrating an order of magnitude speedup. This is an extended version of our previous conference paper [
2
], which described implementation and soundness proofs for Candle. Our HOL4 implementation and automation are new, as are the CakeML benchmarks.
Publisher
Springer Netherlands,Springer Nature B.V
