José A. Alonso
Proving and computing: The infinite pigeonhole principle and countable choice. ~ Zena M. Ariola, Paul Downen, Hugo Herbelin. https://arxiv.org/abs/2603.04006 #RocqProver #ITP
Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice
Structural recursion is a common technique used by programmers in modern languages and is taught to introductory computer science students. But what about its dual, structural corecursion? Structural corecursion is an elegant technique, supported in languages like Haskell and proof assistants such as Rocq or Agda. It enables the design of compositional algorithms by decoupling the generation and consumption of potentially infinite or large data collections. Despite these strengths, structural corecursion is generally considered more advanced than structural recursion and is primarily studied in the context of pure functional programming. Our aim is to illustrate the expressive power of different notions of structural corecursion in the presence of classical reasoning. More specifically, we study coiteration and corecursion combined with the classical callcc operator, which provides a computational interpretation of classical reasoning. This combination enables interesting stream-processing algorithms. As an application, we present a corecursive, control-based proof of the Infinite Pigeonhole Principle and compare it with the continuation-passing proof of Escardó and Oliva in Agda. To further demonstrate the power of mixing corecursion and control, we give an implementation of the Axiom of Countable Choice. In contrast to the usual continuation-passing implementations of this axiom, which rely on general recursion whose termination is established externally, our approach justifies termination by coiteration alone.
Readings shared March 04, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/05-readings_shared_02-04-26 #AI #AI4Math #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #RocqProver
Mechanizing the proof of a borrow calculus. ~ Alban Reynaud Michez. https://hal.science/hal-05527340v1/file/article.pdf #RocqProver #ITP
Readings shared March 01, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/02-readings_shared_02-01-26 #ITP #LeanProver #RocqProver
Bidirectional interpolation for the lambda-calculus – Revisiting and formalising Craig-Čubrić interpolation. ~ Meven Lennon-Bertrand, Alexis Saurin. https://hal.science/hal-05526634v1/file/main.pdf #RocqProver #ITP
Machine-generated, machine-checked proofs for a verified compiler (Experience report). ~ Zoe Paraskevopoulou. https://arxiv.org/abs/2602.20082 #RocqProver #ITP
Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without human proof writing. The proof establishes semantic preservation for the administrative normal form (ANF) transformation in the CertiCoq verified compiler for Rocq. The closely related continuation-passing style (CPS) transformation in CertiCoq was previously proved correct by human experts over several months. We use this proof as a template and instruct the LLM to adapt the proof technique to the ANF setting, which differs in important technical ways. The resulting ANF proof comprises approximately 7,800 lines of Rocq (larger than the 5,300-line CPS proof) and was developed in approximately 96 hours. We describe the proof technique and report on the experience of developing it with an LLM, discussing both the strengths and limitations of the approach and its implications for verified compiler construction.
pesco💯 YES. I did it! 100%-ed Software Foundations, Volume 1: Logical Foundations. Every chapter, every single exercise solved. 
Some parts were a bit of a slog, as is to be expected, but all in all: Yep, had fun up to the very end. 
This means, of course, that I should start on Volume 2 (Programming Foundations) soon. I will busy myself with something else this week and possibly next month, but the plan is to get into it by April. Not another 9 year hiatus!
A Rocq-based formalization of Hilbert’s geometry: Building a reusable foundation for 3D perpendicularity theory and verification. ~ Qimeng Zhang, Wensheng Yu. https://www.mdpi.com/2297-8747/31/1/25 #RocqProver #ITP #Math