License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.4
URN: urn:nbn:de:0030-drops-183797
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18379/
Abrahamsson, Oskar ;
Myreen, Magnus O.
Fast, Verified Computation for Candle
Abstract
This paper describes how we have added an efficient function for computation to the kernel of the Candle interactive theorem prover. Candle is a CakeML port of HOL Light which we have, in prior work, proved sound w.r.t. the inference rules of the higher-order logic. This paper extends the original implementation and soundness proof with a new kernel function for fast computation. Experiments show that the new computation function is able to speed up certain evaluation proofs by several orders of magnitude.
BibTeX - Entry
@InProceedings{abrahamsson_et_al:LIPIcs.ITP.2023.4,
author = {Abrahamsson, Oskar and Myreen, Magnus O.},
title = {{Fast, Verified Computation for Candle}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {4:1--4:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18379},
URN = {urn:nbn:de:0030-drops-183797},
doi = {10.4230/LIPIcs.ITP.2023.4},
annote = {Keywords: Prover soundness, Higher-order logic, Interactive theorem proving}
}
