PONV Daily

Tracking Redexes in the Lambda Calculus

Jean-Jacques Lévy

Residuals of redexes keep track of redexes along reductions in the lambda calculus. Families of redexes keep track of redexes created along these reductions. In this paper, we review these notions and their relation to a labeled λ-calculus introduced here in a systematic way. These properties may be extended to combinatory logic, term rewriting systems, process calculi and proofnets of linear logic.

https://inria.hal.science/hal-03564707/document

Reference counting as a computational interpretation of linear logic

Jawahar Chirimar, Carl A. Gunter and Jon G. Riecke

We develop an operational model for a language based on linear logic. Our semantics is ‘low-level’ enough to express sharing and copying while still being ‘high-level’ enough to abstract away from details of memory layout, and thus can be used to test potential applications of linear logic for analysis of programs. In particular, we demonstrate a precise relationship between type correctness for the linear-logic-based language and the correctness of a reference-counting interpretation of the primitives, and formulate and prove a result describing the possible run-time reference counts of values of linear type.

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/reference-counting-as-a-computational-interpretation-of-linear-logic/57AE85B618932EE0D716556774E73904

После лекции про System T меня расспрашивали про доказательства непротиворечивости и теоремы о неполноте. Я решил написать обзор про теоремы Гёделя, программу Гильберта — как мы понимаем их сейчас и как я вижу куда надо двигаться дальше.

5 страниц + библиография, по-русски. Комментарии и поправки приветствуются.

https://dl.acm.org/doi/epdf/10.1145/2544173.2509546 Carbin, Misailovic, Rinard, [2013] "Verifying Quantitative Reliability for Programs That Execute on Unreliable Hardware"

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://pages.cs.wisc.edu/~remzi/Naur.pdf Naur, [1985] "Programming as theory building"

Dynamic Programming, volume 2

https://dp.quantecon.org/

"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/