#hol4 — Public Fediverse posts

Readings 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

Readings shared September 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/09/24-readings_shared_09-23-25 #Abella #Agda #CategoryTheory #CoqProver #FunctionalProgramming #HOL4 #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Naproche #Rocq #RustLang

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

Readings shared June 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/22-readings_shared_06-21-25 #FunctionalProgramming #HOL4 #Haskell #ITP #IsabelleHOL #LeanProver #Logic #LogicProgramming #Prolog

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

Readings shared April 2, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/02-readings_shared_04-02-25 #FunctionalProgramming #HOL4 #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Mathlib #Prolog

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

Readings shared January 13, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/13-readings_shared_01-13-25 #ITP #Coq #Rocq #HOL4 #CommonLisp #Programming #Math

Proof recommendation system for the HOL4 theorem prover. ~ Nour Dekhil, Adnan Rashid, Sofiene Tahar. https://arxiv.org/abs/2501.05463 #ITP #HOL4

Readings shared September 6, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/06-readings_shared_09-06-24 #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #PVS #Logic #HOL4 #Lisa #Mizar #ACL2 #Math #AI #MachineLearning

A formal proof of R(4,5)=25. ~ Thibault Gauthier & Chad E. Brown. https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.16/LIPIcs.ITP.2024.16.pdf #ITP #HOL4 #Math

Lecturas compartidas el 9 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/10-lecturas_compartidas_el_09-ago-24 #ITP #IsabelleHOL #LeanProver #HOL4 #Coq #Math #Haskell #FunctionalProgramming #IA

Validation of HOL4's formal floating-point model. ~ Hugo Eidmann. https://www.diva-portal.org/smash/get/diva2:1879248/FULLTEXT01.pdf #ITP #HOL4

Lecturas compartidas el 8 de mayo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-8-de-mayo #ITP #Lean4 #IsabelleHOL #HOL_Light #Coq #HOL4 #Math

HOL4P4: Mechanized small-step semantics for P4. ~ Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam. https://dl.acm.org/doi/pdf/10.1145/3649819 #ITP #HOL4

Lecturas compartidas el 3 de abril de 2024. https://jalonso.substack.com/lecturas-compartidas-el-3-de-abril #ITP #LeanProver #IsabelleHOL #Coq #HOL4 #Haskell #LogicProgramming #Prolog #Python #Logic #Math #AI #LLMs #Autoformalization

A formal proof of R(4,5)=25. ~ Thibault Gauthier, Chad E. Brown. https://arxiv.org/abs/2404.01761 #ITP #HOL4 #Math

PureCake: A verified compiler for a lazy functional language. ~ Hrutvik Kanabar et als. https://dl.acm.org/doi/pdf/10.1145/3591259 #ITP #HOL4

A verified theorem prover for higher-order logic. ~ Oskar Abrahamsson. https://research.chalmers.se/publication/532951/file/532951_Fulltext.pdf #PhDThesis #ITP #HOL4