Fast, verified computation for HOL ITPs

DOI10.1007/S10817-025-09719-8MaRDI QIDQ7009612zbMATH OpenFDO

Authors Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Hrutvik Kanabar, Johannes Åman Pohjola

Publication date 20 March 2025

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-025-09719-8

zbMATH Keywords

higher-order logicinteractive theorem provingprover soundness

Mathematics Subject Classification ID

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

Cites work

• (Nominal) unification by recursive descent with triangular substitutions
• A Brief Overview of HOL4
• A compiled implementation of normalisation by evaluation
• A compiled implementation of strong reduction
• CakeML
• Candle: a verified implementation of HOL light
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• Code generation via higher-order rewrite systems
• Fast, verified computation for candle
• HOL Light: An Overview
• scientific article; zbMATH DE number 1670733 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof-producing synthesis of CakeML from monadic HOL functions
• The Lean 4 theorem prover and programming language
• The verified CakeML compiler backend

Cited in

(2)

• Candle: a verified implementation of HOL Light (extended version)
• GOL in GOL in HOL: verified circuits in Conway's game of life

This page was built for publication: Fast, verified computation for HOL ITPs

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