https://link.springer.com/chapter/10.1007/978-3-031-16912-0_3 Hinze, Swierstra, [2022] "Calculating Datastructures"

STRANGE NEW UNIVERSES: PROOF ASSISTANTS AND SYNTHETIC FOUNDATIONS
MICHAEL SHULMAN
Existing computer programs called proof assistants can verify the correctness of mathematical proofs but their specialized proof languages present a barrier to entry for many mathematicians. Large language models have the potential to lower this barrier, enabling mathematicians to interact with proof assistants in a more familiar vernacular. Among other advantages, this may allow mathematicians to explore radically new kinds of mathematics using an LLM-powered proof assistant to train their intuitions as well as ensure their arguments are correct. Existing proof assistants have already played this role for fields such as homotopy type theory

https://www.ams.org/journals/bull/0000-000-00/S0273-0979-2024-01830-8/S0273-0979-2024-01830-8.pdf

ABSTRACTION BOUNDARIES AND SPEC DRIVEN DEVELOPMENT IN PURE MATHEMATICS
JOHAN COMMELIN AND ADAM TOPAZ

In this article we discuss how abstraction boundaries can help tame complexity in mathematical research with the help of an interactive theorem prover. While many of the ideas we present here have been used implicitly by mathematicians for some time, we argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas.

https://www.ams.org/journals/bull/0000-000-00/S0273-0979-2024-01831-X/S0273-0979-2024-01831-X.pdf

https://okmij.org/ftp/tagless-final/datatypes.html

Many examples of tagless-final DSL embedding center on languages with numbers and functions. Occasionally, arrays and lists make an ad hoc appearance. One may, however, want to embed a language with tuples, sums (such as option a.k.a Maybe), as well as various trees. Rather than designing the embedding for each particular data type from scratch, one would ideally apply a general method, almost mechanically. Such general and convenient embedding recipe has been lacking so far.
Examples of ADT embedding in tagless-final style are rare because ADT invariably evoke pattern-matching -- the biggest attraction of ADT -- and pattern-matching in tagless-final style is known to be awkward. Or so I thought.

This article demonstrates a systematic embedding of a language with ADTs, and their recursive processing (constructing, transforming, consuming) using pattern-matching.

My Favorite Math Jokes
Tanya Khovanova

https://arxiv.org/abs/2403.01010

Bruno Gavranović has finally published his thesis 🎉

Fundamental Components of Deep Learning
A category-theoretic approach

https://www.brunogavranovic.com/assets/FundamentalComponentsOfDeepLearning.pdf

A summary is available at: https://www.brunogavranovic.com/posts/2024-03-13-my-thesis-is-out.html

Oxidizing OCaml with Modal Memory Management
A. Lorenzen, L. White, S. Dolan, R. Eisenberg, S. Lindley

https://homepages.inf.ed.ac.uk/slindley/papers/mode-inference-draft-feb2024.pdf

Knuth–Morris–Pratt illustrated
C. Moy

https://www.cambridge.org/core/services/aop-cambridge-core/content/view/8EFA77D663D585B68630E372BCE1EBA4/S0956796824000017a.pdf/div-class-title-knuth-morris-pratt-illustrated-div.pdf

Asymptotic speedup via effect handlers
D. Hillerström, S. Lindley, J. Longley

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/asymptotic-speedup-via-effect-handlers/296879DE2FD96FB6CF388F27978C76E4

From Batch to Stream: Automatic Generation of Online Algorithms

We propose a new technique that converts batch processing programs (i.e., offline algorithms) to their online streaming version that takes one element at a time.
As a cool example, given the standard variance computation for a list of elements (left), our method can automatically generate Welford’s algorithm for online variance computation (right):

https://pbs.twimg.com/media/GMBpnclXcAEh9B9?format=jpg&name=4096x4096

Paper: https://arxiv.org/abs/2404.04743
Code: https://github.com/utopia-group/opera

Merklizing the key/value store for fun and profit


https://docs.canvas.xyz/blog/2023-05-04-merklizing-the-key-value-store.html

Distributed Snapshots: Chandy-Lamport protocol

https://blog.fponzi.me/2024-05-30-distributed-snapshots.html

Control structures
Xavier Leroy
English translation, 2023-2024

https://xavierleroy.org/CdF/2023-2024/index.html

What Goes Around Comes Around... And Around...
M. Stonebraker, A. Pavlo

It took three years to finish, but our follow-up to the 2006 "What Goes Around Comes Around" is finally out! Stonebraker and I examine the last 20 years in databases and discuss why relational databases + SQL will continue to remain on top.

https://db.cs.cmu.edu/papers/2024/whatgoesaround-sigmodrec2024.pdf

https://hal.science/hal-04535159/ Lesbre, Lemerre, [2024] "Compiling with abstract interpretation"