1. Destabilizing Iris (https://doi.org/10.1145/3729284)

2. Tree Borrows (https://doi.org/10.1145/3735592)

3. Principal Type Inference under a Prefix: A Fresh Look at Static Overloading (https://doi.org/10.1145/3729308)

4. Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic (https://doi.org/10.1145/3729246)

5. Practical Type Inference with Levels (https://doi.org/10.1145/3729338)

6. AWDIT: An Optimal Weak Database Isolation Tester (https://doi.org/10.1145/3742465)

Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation

Daniil Berezun
Neil D. Jones

Any expression M in ULC (the untyped λ-calculus) can be compiled into a rather low-level language we call LLL, whose programs contain none of the traditional implementation devices for functional languages: environments, thunks, closures, etc. A compiled program is first-order functional and has a fixed set of working variables, whose number is independent of M. The generated LLL code in effect traverses the subexpressions of M.

We apply the techniques of game semantics to the untyped λcalculus, but take a more operational viewpoint that uses less mathematical machinery than traditional presentations of game semantics. Further, the untyped lambda calculus ULC is compiled into LLL by partially evaluating a traversal algorithm for ULC.

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

Learn you Galois Fields for Great Good

https://xorvoid.com/galois_fields_for_great_good_00.html

Fail Faster: Staging and Fast Randomness for High-Performance PBT

property-based testing - ✅
staging - ✅

https://arxiv.org/abs/2503.19797

video: https://www.youtube.com/watch?v=ux49IvxKQR8

OPLSS 2025

https://www.cs.uoregon.edu/research/summerschool/summer25/topics.php

Functional abstract interpretation

Sebastian Graf

In this thesis, I present two results of my work to improve GHC: the first is a static analysis for pattern-match coverage checking that is both more efficient and more precise than the state of the art; the second is a design pattern for deriving static higher-order analyses and dynamic semantics alike from a generic denotational interpreter, in order to share intuition and correctness proofs. This design pattern generalises Cousot’s seminal work on trace-based abstract interpretation to higher-order analyses such as GHC’s Demand Analysis.

https://simon.peytonjones.org/abs-den/

Dual-Numbers Reverse AD for Functional Array Languages
T. Smelding, M. Konarski, S. PJ, A. Fitzgibbon

https://arxiv.org/abs/2507.12640

A new thing from the database guys from Technical University of Munich. For reference: Thomas Neumann is probably the greatest DB researcher alive. Their Umbra DB is currently top-1 at ClickBench, and its commercial counterpart, CedarDB, takes the 2nd place.

AnyBlox: A Framework for Self-Decoding Datasets
M. Gienieczko, M. Kuschewski, T. Neumann, V. Leis, J. Giceva

https://gienieczko.com/anyblox-paper

@fizruk31337, @clayrat, возможно я добил вопрос симплициальных типов и направленных алгебраических теорий: https://akuklev.github.io/reedy.pdf

Наконец-то десять лет работы сложились в целостную картину.

On the Theoretical Limitations of Embedding-Based Retrieval
O. Weller, M. Boratko, I. Naim, J. Lee

https://arxiv.org/abs/2508.21038

Да, кстати, ведение в бесконечность-категории написанное инвариантным языком: https://runegha.folk.ntnu.no/naivecat_web.pdf

Чистое и содержательное. Возможно, лучший вводный текст на сегодняшний день (написан весной 2025). Узнал о нём от Игната.

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

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!

Some Scala, for a change of pace. You may still remember the language.

https://kubuszok.com/2025/sanely-automatic-derivation/

Hyperfunctions: Communicating Continuations
D. Kidney, N. Wu

https://doisinkidney.com/pdfs/hyperfunctions.pdf

Functional Data Structures and Algorithms
ed. by T. Nipkow

https://fdsa-book.net/