MetaOCaml: Ten Years Later
Oleg

https://okmij.org/ftp/meta-programming/design-10.pdf
https://okmij.org/ftp/ML/MetaOCaml.html#design-10

You could have invented Fenwick trees
B. Yorgey

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/you-could-have-invented-fenwick-trees/B4628279D4E54229CED97249E96F721D

https://vezwork.github.io/drostes-lair-post/

A cute cool project. If you don't understand recursion, this can help immensely. Also if you don't know what the amb is, you can and should learn.

If you already know all that, it's just a fun game. 😊

Eratosthenes again.

Turner, Bird, Eratosthenes: An eternal burning thread
by J. Gibbons

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/turner-bird-eratosthenes-an-eternal-burning-thread/32E2EDF5D5EAEC95F13D313BC97B86F0

Learn Programming with OCaml
by Sylvain Conchon and Jean-Christophe Filliâtre, 2025

https://usr.lmf.cnrs.fr/lpo/

https://calculatingempires.net/

A fascinating visualization (a timeline) of the development of communication, data management, computing, education, medicine, economy, energy, policy, surveillance, military and so on from 1500 till today across the world.

I'm not sure it's 100% historically accurate, but still illuminating.

https://www.youtube.com/watch?v=CVLSA8YGvM8

https://catcolab.org (https://github.com/ToposInstitute/CatColab)

This is mind-blowing! 🤯

A collaborative (as in Google Docs) notebook for defining and simulating a range of "logic"/diagram notations starting with purely descriptive ontologies and up to quantitative stock-and-flow diagrams (which define a system of differential equations).

Implemented in Rust and TypeScript offloading the heavy-lifting of actual processing to AlgebraicJulia and Julia's differential equations ecosystem. All based on Double Category Theory.

https://arxiv.org/abs/2502.03544
Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V. Le, Thang Luong
5 Feb 2025

We present AlphaGeometry2, a significantly improved version of AlphaGeometry introduced in Trinh et al. (2024), which has now surpassed an average gold medalist in solving Olympiad geometry problems. To achieve this, we first extend the original AlphaGeometry language to tackle harder problems involving movements of objects, and problems containing linear equations of angles, ratios, and distances. This, together with other additions, has markedly improved the coverage rate of the AlphaGeometry language on International Math Olympiads (IMO) 2000-2024 geometry problems from 66% to 88%. The search process of AlphaGeometry2 has also been greatly improved through the use of Gemini architecture for better language modeling, and a novel knowledge-sharing mechanism that combines multiple search trees. Together with further enhancements to the symbolic engine and synthetic data generation, we have significantly boosted the overall solving rate of AlphaGeometry2 to 84% for all geometry problems over the last 25 years, compared to 54% previously. AlphaGeometry2 was also part of the system that achieved silver-medal standard at IMO 2024. Last but not least, we report progress towards using AlphaGeometry2 as a part of a fully automated system that reliably solves geometry problems directly from natural language input.

https://dl.acm.org/doi/10.1145/3704912
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter

Proof assistants based on dependent type theory, such as Coq, Lean and Agda, use different universes to classify types, typically combining a predicative hierarchy of universes for computationally-relevant types, and an impredicative universe of proof-irrelevant propositions. In general, a universe is characterized by its sort, such as Type or Prop, and its level, in the case of a predicative sort. Recent research has also highlighted the potential of introducing more sorts in the type theory of the proof assistant as a structuring means to address the coexistence of different logical or computational principles, such as univalence, exceptions, or definitional proof irrelevance. This diversity raises concrete and subtle issues from both theoretical and practical perspectives. In particular, in order to avoid duplicating definitions to inhabit all (combinations of) universes, some sort of polymorphism is needed. Universe level polymorphism is well-known and effective to deal with hierarchies, but the handling of polymorphism between sorts is currently ad hoc and limited in all major proof assistants, hampering reuse and extensibility. This work develops sort polymorphism and its metatheory, studying in particular monomorphization, large elimination, and parametricity. We implement sort polymorphism in Coq and present examples from a new sort-polymorphic prelude of basic definitions and automation. Sort polymorphism is a natural solution that effectively addresses the limitations of current approaches and prepares the ground for future multi-sorted type theories.

TL;DR: do not use LLMs for forecasting.

https://arxiv.org/abs/2406.16964

Termination Combinators Forever
Maximilian Bolingbroke, Simon Peyton Jones, Dimitrios Vytiniotis

We describe a library-based approach to constructing termination tests suitable for controlling termination of symbolic methods such as partial evaluation, supercompilation and theorem proving. With our combinators, all termination tests are correct by construction. We show how the library can be designed to embody various optimisations of the termination tests, which the user of the library takes advantage of entirely transparently.

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/termination-combinators.pdf

https://www.pm.inf.ethz.ch/research/verifythis.html

Another VerifyThis Competition is coming May 3rd and 4th, 2025.

Online participants are welcome: https://docs.google.com/forms/d/e/1FAIpQLScOhK5tMG5q5DMb36yrTQ8itUwvJ2EN8IG_kgjsX6HQZ6dDhw/viewform

The use of AI-based tools is allowed.

Programming Really Is Simple Mathematics
B. Meyer, R. Weber

https://arxiv.org/abs/2502.17149

https://corticallabs.com/cl1.html

A brain in a vat, but unironically... 🥴

Zero copy data structures

https://www.hytradboi.com/2025/df37d71b-0552-47f9-af36-f53c9ee09f8f-zero-copy-data-structures

Keep an eye on the conference, https://www.hytradboi.com/2025

Dear readers, you probably want to be subscribed to these link aggregator channels. Reading them for a few years, heartily recommend.

- https://www.tg-me.com/axisofordinary
- https://www.tg-me.com/j_links