Scholarlink

<p>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 [<CitationRef CitationID="CR2">2</CitationRef>], which described implementation and soundness proofs for Candle. Our HOL4 implementation and automation are new, as are the CakeML benchmarks.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Fast, Verified Computation for HOL ITPs

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年2月18日

查看全文
  • Oskar Abrahamsson,
  • Magnus O. Myreen,
  • Michael Norrish,
  • Hrutvik Kanabar,
  • Johannes Åman Pohjola

摘要

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.