👍5❤🔥4🤯2🌚1
Understanding Random Forests: From Theory to Practice, thesis
G. Louppe
https://arxiv.org/abs/1407.7502
G. Louppe
https://arxiv.org/abs/1407.7502
🫡3👍1😁1
Grokking as Compression: A Nonlinear Complexity Perspective
Z. Liu, Z. Zhong, M. Tegmark
https://arxiv.org/abs/2310.05918
Z. Liu, Z. Zhong, M. Tegmark
https://arxiv.org/abs/2310.05918
😴1
Quotient Haskell, Lightweight Quotient Types for All
B. Hewer, G. Hutton
Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting Quotient Haskell, an extension of Liquid Haskell with support for quotient types.
https://www.cs.nott.ac.uk/~pszgmh/quotient-haskell.pdf
B. Hewer, G. Hutton
Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting Quotient Haskell, an extension of Liquid Haskell with support for quotient types.
https://www.cs.nott.ac.uk/~pszgmh/quotient-haskell.pdf
🥴2
Capturing Types
https://dl.acm.org/doi/abs/10.1145/3618003
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties
could be guaranteed if one knew the free variables captured by values. We describe
variables are succinctly represented in types, and show it can be used to safely implement efects and efect polymorphism via
scoped capabilities. We discuss how the decision to track captured variables guides key aspects of the calculus, and show that
these ideas can be used to guide the implementation of capture checking in a practical programming language.
https://dl.acm.org/doi/abs/10.1145/3618003
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties
could be guaranteed if one knew the free variables captured by values. We describe
CC<:□ , a calculus where such capturedvariables are succinctly represented in types, and show it can be used to safely implement efects and efect polymorphism via
scoped capabilities. We discuss how the decision to track captured variables guides key aspects of the calculus, and show that
CC<:□ admits simple and intuitive types for common data structures and their typical usage patterns. We demonstrate howthese ideas can be used to guide the implementation of capture checking in a practical programming language.
👍2💅2
Forwarded from ∫f(x)dx
❤2👌1🥴1
Пародийная песня "The Telnet Song" за авторством Guy Steele была опубликована в Communications of the ACM в апреле 1984 года:
https://dl.acm.org/doi/pdf/10.1145/358027.1035691
https://dl.acm.org/doi/pdf/10.1145/358027.1035691
👍1👎1😁1
🤝4
Advent of Code comes to an end, here's some recreational math for your Christmas and New Year holidays
https://kam.mff.cuni.cz/~matousek/stml-53-matousek-1.pdf
https://kam.mff.cuni.cz/~matousek/stml-53-matousek-1.pdf
👍2👌2
Forwarded from ∫f(x)dx
чет даже никто не скинул https://www.youtube.com/@acmsigplan
Forwarded from Sergey Kucherenko
🔥1
The Functional Essence of Imperative Binary Search Trees
Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced. This paper presents several novel functional algorithms for accessing and inserting elements in a restructuring binary search tree that are as fast as their imperative counterparts; yet the correctness of these functional algorithms is established using a simple inductive argument. For each data structure, move-to-root, splay, and zip trees, this paper describes both a bottom-up algorithm using zippers and a top-down algorithm using a novel first-class constructor context primitive. The functional and imperative algorithms are equivalent: we mechanise the proofs establishing this in the Coq proof assistant using the Iris framework. This yields a first fully verified implementation of well known algorithms on binary search trees with performance on par with the fastest implementations in C.
https://www.microsoft.com/en-us/research/uploads/prod/2023/07/fiptree-tr-v4.pdf
Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced. This paper presents several novel functional algorithms for accessing and inserting elements in a restructuring binary search tree that are as fast as their imperative counterparts; yet the correctness of these functional algorithms is established using a simple inductive argument. For each data structure, move-to-root, splay, and zip trees, this paper describes both a bottom-up algorithm using zippers and a top-down algorithm using a novel first-class constructor context primitive. The functional and imperative algorithms are equivalent: we mechanise the proofs establishing this in the Coq proof assistant using the Iris framework. This yields a first fully verified implementation of well known algorithms on binary search trees with performance on par with the fastest implementations in C.
https://www.microsoft.com/en-us/research/uploads/prod/2023/07/fiptree-tr-v4.pdf
🔥5
The Structure of Meaning in Language: Parallel Narratives in Linear Algebra and Category Theory
https://www.ams.org/journals/notices/202402/rnoti-p174.pdf
https://www.ams.org/journals/notices/202402/rnoti-p174.pdf
https://www.cs.ru.nl/B.Jacobs/PAPERS/ProbabilisticReasoning.pdf Jacobs, [2023] "Structured Probabilistic Reasoning"