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