Anyway, I'll allow myself to advertise Valera's course on constructive mathematics. It is available online at https://www.youtube.com/watch?v=EHYiB19EYFs&list=PLRtkLMXefuh8EiRRuc7Uz-k6NKIIWHJf8

However, probably some knowledge of Russian is required.

Новая версия
Polynomial Functors: A Mathematical Theory of Interaction
https://arxiv.org/abs/2312.00990
Что там, не смотрел, но скорее всего, что исправления мелких багов.

Concurrent Data Structures Made Easy
C. Le, K. Gopinathan, K. Wen Lee, S. Gilbert, I. Sergey.

https://ilyasergey.net/assets/pdf/papers/obatcher-oopsla24.pdf
https://github.com/verse-lab/obatcher_ds/tree/paper-artefact

https://x.com/ilyasergey/status/1829026676623454661

Soundly Handling Linearity
W. Tang, D. Hillerström, S. Lindley, and J. G. Morris

https://blog.sigplan.org/2024/08/12/soundly-handling-linearity/

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

Swift: Error Handling Rationale

https://github.com/swiftlang/swift/blob/9315673c003875158852579bd1f33480cdec5461/docs/ErrorHandlingRationale.md#fundamentals

https://stringdiagram.com/wp-content/uploads/2024/08/graphicaltheoryofmonadsv2.0.pdf

The graphical theory of monads
R. Hinze, D. Marsden

Warning: requires some background, not a monad tutorial.

Capabilities for Control — ICFP 2024
M. Odersky

https://www.youtube.com/live/F70QZaMoYJQ?feature=shared&t=2090

34:50

What is Entropy?
John C. Baez, 2024

https://arxiv.org/pdf/2409.09232

The authors show that, with the right algorithmic enhancements, first-order methods(*) can be competitive with state-of-the-art Linear Programming solvers, even for problems requiring high-accuracy solutions. This opens up new possibilities and computational trade-offs when solving LP problems, especially for large-scale instances.

* In numerical analysis, methods that have at most linear local error are called first order methods.

Blog: https://research.google/blog/scaling-up-linear-programming-with-pdlp/

Paper (go read the blog for intro): https://www.openread.academy/en/paper/reading?corpusId=235376806

Modular Borrowing Without Ownership or Linear Types
L. Parreaux
https://2024.splashcon.org/details/iwaco-2024-papers/5/Modular-Borrowing-Without-Ownership-or-Linear-Types

A Science of Concurrent Programs (2024)

L. Lamport

https://lamport.azurewebsites.net/tla/science.pdf

Cloud-Native Database Systems and Unikernels: Reimagining OS Abstractions for Modern Hardware
V. Leis, C. Dietrich

https://www.vldb.org/pvldb/vol17/p2115-leis.pdf

FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI

We introduce FrontierMath, a benchmark of hundreds of original, exceptionally challenging mathematics problems crafted and vetted by expert mathematicians. The questions cover most major branches of modern mathematics -- from computationally intensive problems in number theory and real analysis to abstract questions in algebraic geometry and category theory. Solving a typical problem requires multiple hours of effort from a researcher in the relevant branch of mathematics, and for the upper end questions, multiple days. FrontierMath uses new, unpublished problems and automated verification to reliably evaluate models while minimizing risk of data contamination. Current state-of-the-art AI models solve under 2% of problems, revealing a vast gap between AI capabilities and the prowess of the mathematical community. As AI systems advance toward expert-level mathematical abilities, FrontierMath offers a rigorous testbed that quantifies their progress.

https://arxiv.org/abs/2411.04872

https://doisinkidney.com/posts/2024-11-08-formalising-graphs-coinduction.html

Formalising Graphs with Coinduction
D. Kidney, N. Wu

All that said, I think the representation we ended up with in the paper is quite nice. We start with a similar representation to the one we had in our ICFP paper in 2021: a graph over vertices of type a is simply a function a -> [a] that returns the neighbours of a supplied vertex (this is the same representation as in this post). Despite the simplicity, it turns out that this type is enough to implement a decent number of search algorithms. The really interesting thing is that the arrow methods (from Control.Arrow) work on this type, and they define an algebra on graphs similar to the one from Mokhov (2017). For example, the <+> operator is the same as the overlay operation in Mokhov (2017).

That simple type gets expanded upon and complicated: eventually, we represent a possibly-infinite collection as a function that takes a depth and then returns everything in the search space up to that depth.

The Denotational Semantics of SSA

J. Ghalayini, N. Krishnaswami

Static single assignment form, or SSA, has been the dominant compiler intermediate representation for decades. In this paper, we give a type theory for a variant of SSA, including its equational theory, which are strong enough to validate a variety of control and data flow transformations. We also give a categorical semantics for SSA, and show that the type theory is sound and complete with respect to the categorical axiomatization. We demonstrate the utility of our model by exhibiting a variety of concrete models satisfying our axioms, including in particular a model of TSO weak memory. The correctness of the syntactic metatheory, as well as the completeness proof has been mechanized in the Lean proof assistant.

https://arxiv.org/abs/2411.09347