Staged Compilation with Two-Level Type Theory
https://www.inf.elte.hu/dstore/document/2582/tkp_2023_01_18_prez_Kov%C3%A1cs_A.pdf
https://www.inf.elte.hu/dstore/document/2582/tkp_2023_01_18_prez_Kov%C3%A1cs_A.pdf
๐1
Distillation: extracting the essence of programs
https://www.semanticscholar.org/paper/Distillation%3A-extracting-the-essence-of-programs-Hamilton/08871ba7e80525327ba4404ea41ccaf6aa18187d
https://www.semanticscholar.org/paper/Distillation%3A-extracting-the-essence-of-programs-Hamilton/08871ba7e80525327ba4404ea41ccaf6aa18187d
๐1๐ฅ1
A 100x speedup with unsafe Python
https://yosefk.com/blog/a-100x-speedup-with-unsafe-python.html
https://yosefk.com/blog/a-100x-speedup-with-unsafe-python.html
Results of the Grand C++ Error Explosion Competition
https://www.tumblr.com/tgceec/74534916370/results-of-the-grand-c-error-explosion
https://www.tumblr.com/tgceec/74534916370/results-of-the-grand-c-error-explosion
Tumblr
Post by @tgceec
๐ฌ 0 ๐ 167 โค๏ธ 196 ยท Results of the Grand C++ Error Explosion Competition ยท After much deliberation, the winners of the Grand C++ Error Explosion Competition are finally selected. There are two difโฆ
A Simple and Efficient Implementation of Strong Call by Need by an Abstract Machine
https://dl.acm.org/doi/pdf/10.1145/3549822
https://dl.acm.org/doi/pdf/10.1145/3549822
Implementing term rewriting by jungle evaluation
https://www.rairo-ita.org/articles/ita/pdf/1991/05/ita1991250504451.pdf
https://www.rairo-ita.org/articles/ita/pdf/1991/05/ita1991250504451.pdf
Introduction to Homotopy Type Theory
https://arxiv.org/abs/2212.11082
https://arxiv.org/abs/2212.11082
arXiv.org
Introduction to Homotopy Type Theory
This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and...
๐ฅ2
Taming Code Explosion in Supercompilation
https://www.diva-portal.org/smash/get/diva2:1013417/FULLTEXT01.pdf
https://www.diva-portal.org/smash/get/diva2:1013417/FULLTEXT01.pdf
๐2
A multi-level tensor algebra superoptimizer
https://github.com/mirage-project/mirage
https://github.com/mirage-project/mirage
GitHub
GitHub - mirage-project/mirage: Mirage: Automatically Generating Fast GPU Kernels without Programming in Triton/CUDA
Mirage: Automatically Generating Fast GPU Kernels without Programming in Triton/CUDA - mirage-project/mirage
๐1
Supercompilation of Double Interpretation (How One Hour of the Machine's Time Can Be Turned to One Second)
http://refal.net/~korlukov/scp2int/Karliukou_Nemytykh.pdf
http://refal.net/~korlukov/scp2int/Karliukou_Nemytykh.pdf
๐1
Optimizing Clickhouse: The Tactics That Worked for Us
https://www.highlight.io/blog/lw5-clickhouse-performance-optimization
https://www.highlight.io/blog/lw5-clickhouse-performance-optimization
Highlight
Optimizing Clickhouse: The Tactics That Worked for Us
highlight.io is the open source monitoring platform that gives you the visibility you need.
๐1
Exploring GNU extensions in the Linux kernel
https://maskray.me/blog/2024-05-12-exploring-gnu-extensions-in-linux-kernel
https://maskray.me/blog/2024-05-12-exploring-gnu-extensions-in-linux-kernel
MaskRay
Exploring GNU extensions in the Linux kernel
The Linux kernel is written in C, but it also leverages extensions provided by GCC. In 2022, it moved from GCC/Clang -std=gnu89 to -std=gnu11. This article explores my notes on how these GNU extension
๐1
Translation of the Rust's core and alloc crates to Coq for formal verification
https://formal.land/blog/2024/04/26/translation-core-alloc-crates
https://formal.land/blog/2024/04/26/translation-core-alloc-crates
formal.land
๐ฆ Translation of the Rust's core and alloc crates | Formal Land
We continue our work on formal verification of Rust programs with our tool coq-of-rust, to translate Rust code to the formal proof system Coq. One of the limitation we had was the handling of primitive constructs from the standard library of Rust, like Oโฆ
๐2