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.

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.tgoop.com/axisofordinary
- https://www.tgoop.com/j_links

The Functional Machine Calculus

Willem Heijltjes

This paper presents the Functional Machine Calculus (FMC) as a simple model of higher-order computation with "reader/writer" effects: higher-order mutable store, input/output, and probabilistic and non-deterministic computation.

The FMC derives from the lambda-calculus by taking the standard operational perspective of a call-by-name stack machine as primary, and introducing two natural generalizations. One, "locations", introduces multiple stacks, which each may represent an effect and so enable effect operators to be encoded into the abstraction and application constructs of the calculus. The second, "sequencing", is known from kappa-calculus and concatenative programming languages, and introduces the imperative notions of "skip" and "sequence". This enables the encoding of reduction strategies, including call-by-value lambda-calculus and monadic constructs.

https://arxiv.org/abs/2212.08177

Collapsing Towers of Interpreters

Nada Amin, Tiark Rompf

Given a tower of interpreters, i.e., a sequence of multiple interpreters interpreting one another as input programs, we aim to collapse this tower into a compiler that removes all interpretive overhead and runs in a single pass. In the real world, a use case might be Python code executed by an x86 runtime, on a CPU emulated in a JavaScript VM, running on an ARM CPU. Collapsing such a tower can not only exponentially improve runtime performance, but also enable the use of base-language tools for interpreted programs, e.g., for analysis and verification. In this paper, we lay the foundations in an idealized but realistic setting.

https://dl.acm.org/doi/10.1145/3158140

Specializing Data Access in a Distributed File System (Generative Pearl)
P. Das, A. Xhebraj, T. Rompf

https://dl.acm.org/doi/10.1145/3689484.3690736

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

Modern distributed file systems partition and replicate data amongst a cluster of participating nodes to enable processing of larger-than-memory datasets and to provide fault tolerance. Typically, these systems maintain designated coordinator nodes that track the state of the cluster and route user operations to the nodes holding the requested data.

One way to improve performance in this scenario is to provide the client with the cluster topology and data distribution information so that they can bypass the designated coordinator and directly access the data. Click Me Load More the files from the underlying file system instead of having to go through high level APIs can lead to significantly better performance <...>

In this paper, we propose a system, DDLoader, that embeds the information about the data distribution into the language using the Lightweight Modular Staging metaprogramming framework for Scala. Multi-stage programming techniques allow developers to build applications while delegating the task of generating low-level file loading details to the generated code. This hides the implementation details of the underlying distributed file system while retaining the performance of handwritten examples. Further, metaprogramming erases the distinction between the data loading and data processing phases of the applications typically built over distributed file systems, allowing whole program optimization, which was not possible previously.

FP²: Fully in-Place Functional Programming

Anton Lorenzen, Daan Leijen, Wouter Swierstra

As functional programmers we always face a dilemma: should we write purely functional code, or sacrifice purity for efficiency and resort to in-place updates? This paper identifies precisely when we can have the best of both worlds: a wide class of purely functional programs can be executed safely using in-place updates without requiring allocation, provided their arguments are not shared elsewhere.

We describe a linear _fully in-place_ (FIP) calculus where we prove that we can always execute such functions in a way that requires no (de)allocation and uses constant stack space. Of course, such a calculus is only relevant if we can express interesting algorithms; we provide numerous examples of in-place functions on datastructures such as splay trees or finger trees, together with in-place versions of merge sort and quick sort.

We also show how we can generically derive a map function over _any_ polynomial data type that is fully in-place. Finally, we have implemented the rules of the FIP calculus in the Koka language. Using the Perceus reference counting garbage collection, this implementation dynamically executes FIP functions in-place whenever possible.

https://dl.acm.org/doi/abs/10.1145/3607840

Denotational design with type class morphisms

Conal Elliott

Type classes provide a mechanism for varied implementations of standard interfaces. Many of these interfaces are founded in mathematical tradition and so have regularity not only of types but also of properties (laws) that must hold. Types and properties give strong guidance to the library implementor, while leaving freedom as well. Some of this remaining freedom is in how the implementation works, and some is in what it accomplishes.

To give additional guidance to the what, without impinging on the how, this paper proposes a principle of type class morphisms (TCMs), which further refines the compositional style of denotational semantics. The TCM idea is simply that the instance’s meaning is the meaning’s instance. This principle determines the meaning of each type class instance, and hence defines correctness of implementation. It also serves to transfer laws about a type’s semantic model, such as the class laws, to hold for the type itself. In some cases, it also provides a systematic guide to implementation, and in some cases, valuable design feedback.

The paper is illustrated with several examples of types, meanings, and morphisms.

http://conal.net/papers/type-class-morphisms/