José A. AlonsoReadings shared December 9, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/10-readings_shared_12-09-25 #AI #FunctionalProgramming #HOL4 #HOL-Light #Haskell #ITP #IsabelleHOL #LeanProver #Math
Candle: A verified implementation of HOL Light. ~ Oskar Abrahamsson et als. https://link.springer.com/article/10.1007/s10817-025-09743-8 #ITP #HOL4 #HOL_Light
Candle: A Verified Implementation of HOL Light (Extended Version) - Journal of Automated Reasoning
This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. Throughout this work, we have strived to make the REPL of the new system provide a user experience as close to HOL Light’s as possible. To this end, we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of the work described in this paper has been carried out in the HOL4 theorem prover.
Mechanising Böhm trees and λη-completeness. ~ Chun Tian and Michael Norrish. https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.28/LIPIcs.ITP.2025.28.pdf #ITP #HOL4
GOL in GOL in HOL: Verified circuits in Conway’s game of life. ~ Magnus O. Myreen and Mario Carneiro. https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.25/LIPIcs.ITP.2025.25.pdf #ITP #HOL4
A verified cost model for call-by-push-value. ~ Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah. https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.7/LIPIcs.ITP.2025.7.pdf #ITP #HOL4
Certifying projected knowledge compilation. ~ Randal E. Bryant, Yong Kiam Tan, Marijn J. H. Heule. https://www.cs.cmu.edu/~mheule/publications/scpog-SAT25.pdf #ITP #HOL4
GOL in GOL in HOL: Verified circuits in Conway's game of life. ~ Magnus O. Myreen, Mario Carneiro. https://arxiv.org/abs/2504.00263 #ITP #HOL4
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life
Conway's Game of Life (GOL) is a cellular automaton that has captured the interest of hobbyists and mathematicians alike for more than 50 years. The Game of Life is Turing complete, and people have been building increasingly sophisticated constructions within GOL, such as 8-bit displays, Turing machines, and even an implementation of GOL itself. In this paper, we report on a project to build an implementation of GOL within GOL, via logic circuits, fully formally verified within the HOL4 theorem prover. This required a combination of interactive tactic proving, symbolic simulation, and semi-automated forward proof to assemble the components into an infinite circuit which can calculate the next step of the simulation while respecting signal propagation delays. The result is a verified "GOL in GOL compiler" which takes an initial GOL state and returns a mega-cell version of it that can be passed to off-the-shelf GOL simulators, such as Golly. We believe these techniques are also applicable to other cellular automata, as well as for hardware verification which takes into account both the physical configuration of components and wire delays.