PONV Daily

Low-Level Software Security for Compiler Developers https://llsoftsec.github.io/llsoftsecbook/

People in the know say it's a daily-worth material, https://youtu.be/FTmmG3Dx8HA

Intrinsically Correct Algorithms and Recursive Coalgebras Cass Alexandru, Henning Urbat, Thorsten Wißmann Recursive coalgebras provide an elegant categorical tool for modelling recursive algorithms and analysing their termination and correctness. By considering coalgebras over categories of suitably indexed families, the correctness of the corresponding algorithms follows intrinsically just from the type of the computed maps. However, proving recursivity of the underlying coalgebras is non-trivial, and proofs are typically ad hoc. This layer of complexity impedes the formalization of coalgebraically defined recursive algorithms in proof assistants. We introduce a framework for constructing coalgebras which are intrinsically recursive in the sense that the type of the coalgebra guarantees recursivity from the outset. Our approach is based on the novel concept of a well-founded functor on a category of families indexed by a well-founded relation. We show as our main result that every coalgebra for a well-founded functor is recursive, and demonstrate that well-known techniques for proving recursivity and termination such as ranking functions are subsumed by this abstract setup https://dl.acm.org/doi/abs/10.1145/3808309

https://yangzhixuan.github.io/NbE.html Yang, [2026] "An Algorithmic Reconstruction of Normalisation by Evaluation"

A Very Elementary Introduction to Sheaves M. Agrios, 2022 https://arxiv.org/abs/2202.01379

От этой папиры весь тви писается: https://arxiv.org/abs/2603.21852

The Discoveries of Continuations John Reynolds https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/reynolds-discoveries.pdf

https://khoury.northeastern.edu/~cmartens/papers/plateau26-itfp.pdf Martens, Tosch, Semenova, Li, [2026] "Is truth futureproof? : On the possible futures of mechanized proofs" https://khoury.northeastern.edu/~cmartens/talks/plateau-itfp-talk-slides.pdf

https://mchav.github.io/what-category-theory-teaches-us-about-dataframes/

https://pages.cs.wisc.edu/~remzi/Naur.pdf Naur, [1985] "Programming as theory building"

Dynamic Programming, volume 2 https://dp.quantecon.org/

https://www-cs-faculty.stanford.edu/~knuth/papers/claude-cycles.pdf

"Package Managers à la Carte, A Formal Model of Dependency Resolution" https://arxiv.org/pdf/2602.18602

I've been carrying this little category theory library around for ten years, porting it from language to language, and every time, the experience tells me something about the state of the art. https://www.stephendiehl.com/posts/lean-opus-blog/

1.11 is out!

Functional Data Structures and Algorithms ed. by T. Nipkow https://fdsa-book.net/

Hyperfunctions: Communicating Continuations D. Kidney, N. Wu https://doisinkidney.com/pdfs/hyperfunctions.pdf

Some Scala, for a change of pace. You may still remember the language. https://kubuszok.com/2025/sanely-automatic-derivation/

Passing the mic to Xavier Leroy: I am happy to announce that a draft of my upcoming book “Control structures in programming languages: from goto to algebraic effects” is now available at https://xavierleroy.org/control-structures . The book compares several programming languages from the standpoint of control structures. OCaml is used intensively to discuss control in functional programming, including continuation-passing style, control operators, exceptions, user-defined effects and effect handlers, with many examples that I hope you’ll like. The book also discusses in depth a number of questions that are often raised in this forum, such as the theory and practice of algebraic effects and handlers, and the static checking of exceptions and effects. Enjoy!

And in the WASM world: typed continuations are in, as per this spec.