Proving binge continues. My regex matching function that has never been called is correct!

This finishes chapter "IndProp" (Inductive Propositions) of #softwarefoundations and that means I am now fully caught up in terms of chapters with where I left it all those years ago - major milestone!

IndProp is also by far the heftiest chapter in Volume 1, so... not far now.

#coq #rocqprover

Readings shared January 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/25-readings_shared_01-24-26 #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver

The HOL-Light library of multivariate real analysis in Rocq. ~ Claudio Sacerdoti Coen, Abdelghani Alidra, Frédéric Blanqui. https://inria.hal.science/hal-05464922/file/Reusing_HOLLight_library_in_Rocq-7.pdf #ITP #RocqProver #HOL_Light #Math

Formally verified number-theoretic transform. ~ Alix Trieu. https://cic.iacr.org/p/2/4/1 #ITP #RocqProver

Readings shared January 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/20-readings_shared_01-19-26 #AI #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #RocqProver

Broken proofs and broken provers. ~ Lawrence Paulson. https://lawrencecpaulson.github.io/2026/01/15/Broken_proofs.html #ITP #IsabelleHOL #RocqProver #LeanProver

Readings shared January 14, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/15-readings_shared_01-14-26 #AI #Autoformalization #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver

Formal verification for JavaScript regular expressions: A proven mechanized semantics and its applications. ~ Aurèle Barrière, Victor Deng, Clément Pit-Claudel. https://dl.acm.org/doi/pdf/10.1145/3776710 #ITP #RocqProver

Computation-tree semantics: An algorithmic approach to structurally defined relations. ~ Sean Kristian Remond Harbo, Hans Hüttel. https://dl.acm.org/doi/pdf/10.1145/3779209.3779534 #ITP #RocqProver

Computing solutions for systems of multivariate ordinary differential equations in Rocq. ~ Holger Thies- https://dl.acm.org/doi/pdf/10.1145/3779031.3779097 #ITP #RocqProver

Readings shared May 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/23-readings_shared_05-23-25 #AIforCode #CategoryTheory #ITP #IsabelleHOL #LLMs #LeanProver #Math #RocqProver

Solving guarded domain equations in presheaves over ordinals and mechanizing it. ~ Sergei Stepanenko, Amin Timany. https://tildeweb.au.dk/au571806/publications/files/2025-fscd-guarded-dom.pdf #ITP #RocqProver #CategoryTheory