Google Keep
Export Method: Highlight, select copy to google doc.
2024-08
| What’s the right way to QuickCheck floating-point routines? | blog :: Brent -> [String] |
https://byorgey.wordpress.com/2019/02/24/whats-the-right-way-to-quickcheck-floating-point-routines/
https://dl.acm.org/doi/pdf/10.1145/177492.177726
Tla plus paper
[2405.18341] The Ross-Darboux-Stieltjes Integral
https://arxiv.org/abs/2405.18341
Barycentric interpolation via the AAA algorithm
http://guettel.com/rktoolbox/examples/html/example_aaa.html
https://people.maths.ox.ac.uk/trefethen/nak_sete_tref_revised.pdf
Aaa algorthm for rational approximation
| CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs | Proceedings of the ACM on Programming Languages |
https://dl.acm.org/doi/10.1145/3674653
https://github.com/yihozhang/Halide/tree/yihozhang-eqsat-roundtrip/src/egglog
Bits, Math and Performance(?)
http://bitmath.blogspot.com/search?updated-max=2023-04-12T17:11:00-07:00&max-results=20
Cool automated bit math identity finding
https://microsoft.github.io/z3guide/programming/Proof%20Logs/
https://news.ycombinator.com/item?id=41322758 Python’s Preprocessor (pydong.org) codec abuse
https://news.ycombinator.com/item?id=41315359 SIMD Matters: Graph Coloring (box2d.org)
https://iopscience.iop.org/article/10.1088/1361-6633/ac03aa/meta
https://www.cl.cam.ac.uk/~jrh13/slides/intel-8jan98/slides.pdf
Harrison floating point of tqng exp
CS 6120: An Interpreter for the btor2 Model Checking Language
https://www.cs.cornell.edu/courses/cs6120/2023fa/blog/btor2i/
MicroZed Chronicles: Beyond Basics—Intermediate FPGA Projects
https://www.adiuvoengineering.com/post/microzed-chronicles-beyond-basics-intermediate-fpga-projects
Measure, Integration & Real Analysis
What Is a Fréchet Derivative? – Nick Higham
https://nhigham.com/2020/06/23/what-is-a-frechet-derivative/
Closed-Form 3x3 Matrix Decompositions
https://theorangeduck.com/page/closed-form-matrix-decompositions
cranberry_blog/StretchyReflections.md at master · AlexSabourinDev/cranberry_blog · GitHub
https://github.com/AlexSabourinDev/cranberry_blog/blob/master/StretchyReflections.md
Serverless AI Inference with Gemma 2 using Mozilla’s llamafile on AWS Lambda
Numerical analytic continuation - Wikipedia
https://en.m.wikipedia.org/wiki/Numerical_analytic_continuation
https://www.cl.cam.ac.uk/~jrh13/papers/complex.pdf
Complex polynomial quant elim hol light
ChocoPy: A Programming Language for Compilers Courses
RiscEmu Documentation! — RiscEmu 2.0.0a2 documentation
https://riscemu.readthedocs.io/en/latest/index.html
| Slides | slides |
https://maaslalani.com/slides/
| Exact Polygonal Filtering: Using Green’s Theorem and Clipping for Anti-Aliasing | Hacker News |
https://news.ycombinator.com/item?id=41253461
| Font with Built-In Syntax Highlighting | Hacker News |
https://news.ycombinator.com/item?id=41245159
https://news.ycombinator.com/item?id=41208988
https://markjgillespie.com/Research/harnack-tracing/HarnackTracing.pdf
Hrmaonic function tracing
Harnack’s inequality - Wikipedia
https://en.wikipedia.org/wiki/Harnack%27s_inequality
Poisson kernel - Wikipedia
https://en.wikipedia.org/wiki/Poisson_kernel
[2408.04564] First steps towards Computational Polynomials in Lean
https://arxiv.org/abs/2408.04564
https://people.bath.ac.uk/masjhd/JHD-CA.pdf
Davenport computer algebra
HFT.m
https://www.axler.net/HFT_Math.html
Harmonic function theory mathematica
blog :: Brent -> [String] - Competitive Programming in Haskell: tree path decomposition, part II
https://byorgey.github.io/blog/posts/2024/08/08/TreeDecomposition.html
| ICPP – Running C++ in anywhere like a script | Hacker News |
https://news.ycombinator.com/item?id=41151013
https://ntrs.nasa.gov/api/citations/20205005199/downloads/Intern_presentation_2020%2008-04.pdf
Pvs lemma selection
https://inria.hal.science/hal-01386986/document
Learning based lemma selection blanchette
Category: RISC-v Bytes · Daniel Mangum
https://danielmangum.com/categories/risc-v-bytes/
[2408.01441] Group Theory in Physics: An Introduction with Mathematica
https://arxiv.org/abs/2408.01441
| Streams, Calculational Proofs and Dafny | Hacker News |
https://news.ycombinator.com/item?id=41178596
| Crafting formulas: Lambdas all the way down | Hacker News |
https://news.ycombinator.com/item?id=41169244
Limit inferior and limit superior - Wikipedia
https://link.springer.com/chapter/10.1007/978-3-642-38574-2_12
| Scheduling Model in LLVM | Hacker News |
https://news.ycombinator.com/item?id=41161831
| Debin | Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security |
[1206.6940] Practical Groebner Basis Computation
https://arxiv.org/abs/1206.6940
| Clang vs. Clang | Hacker News |
https://news.ycombinator.com/item?id=41146860
| Primitive Recursive Functions for a Working Programmer | Hacker News |
https://news.ycombinator.com/item?id=41146278
| A Survey of General-purpose Polyhedral Compilers | ACM Transactions on Architecture and Code Optimization |
https://dl.acm.org/doi/abs/10.1145/3674735
https://pat.keldysh.ru/~grechanik/doc/indprover-eqsat-extended.pdf
Codatatype egraph supercompiler russian
https://gitlab.com/feynmanintegrals/fire
| Using computation to teach the properties of the van der Waals fluid | American Journal of Physics | AIP Publishing |
AJP- Computational Physics
https://www.aapt.org/Publications/AJP/Readers/computational_physics.cfm
https://arxiv.org/pdf/2205.00879
Invitation formal power series
| Coinductive Definitions | The n-Category Café |
https://golem.ph.utexas.edu/category/2011/07/coinductive_definitions.html
| Proof by Coinduction | The n-Category Café |
https://golem.ph.utexas.edu/category/2009/09/proof_by_coinduction.html
| SAM 2: Segment Anything in Images and Videos | Hacker News |
https://news.ycombinator.com/item?id=41104523
Freiling’s axiom of symmetry - Wikipedia
https://en.m.wikipedia.org/wiki/Freiling%27s_axiom_of_symmetry
https://www.cs.uwyo.edu/~ruben/static/pdf/acl2r-theory.pdf
reference request - Unification and Gaussian Elimination - Theoretical Computer Science Stack Exchange
https://cstheory.stackexchange.com/questions/12326/unification-and-gaussian-elimination
https://www3.risc.jku.at/education/courses/ss2011/rw/1-intro.pdf
Canonical reduction sustems in symbolic mathemtics
F. Riesz’s theorem - Wikipedia
https://en.wikipedia.org/wiki/F._Riesz%27s_theorem
| Bril: An Intermediate Language for Teaching Compilers | Hacker News |
https://news.ycombinator.com/item?id=41084318
Every VM tutorial you ever studied is wrong (and other compiler/interpreter-related knowledge) · GitHub
https://gist.github.com/o11c/6b08643335388bbab0228db763f99219
https://libisl.sourceforge.io/tutorial.pdf
Isl tutorial polyhedr
| Bril: An Intermediate Language for Teaching Compilers | Hacker News |
https://news.ycombinator.com/item?id=41084318
algebra_with_sympy API documentation
https://gutow.github.io/Algebra_with_Sympy/algebra_with_sympy.html
Towards a new SymPy: part 2 - Polynomials — blog documentation
https://oscarbenjamin.github.io/blog/czi/post2.html
LLL and sympy
https://groups.google.com/g/sympy/c/X8RjnLr2gOU
Building Lattice Reduction (LLL) Intuition – kel.bz
https://goens.org/publications/fernandez-mir-cicm-24/cicm24.pdf
Unification semuring solving
Recursion theory on the reals and continuous-time computation - ScienceDirect
https://www.sciencedirect.com/science/article/pii/0304397595002480
| What is Entropy? | Azimuth |
https://johncarlosbaez.wordpress.com/2024/07/20/what-is-entropy/
NCAlgebra Homepage: NonCommutative Algebra Software and Examples.
https://mathweb.ucsd.edu/~ncalg/
An introduction to commutative and noncommutative Gröbner bases - ScienceDirect
https://www.sciencedirect.com/science/article/pii/0304397594902836
Word Processing in Groups - Wikipedia
https://en.wikipedia.org/wiki/Word_Processing_in_Groups
Computation with Finitely Presented Groups
[WSRP24] Monoids, String-Rewriting, Confluence, and the Knuth-Bendix Algorithm - Online Technical Discussion Groups—Wolfram Community
https://community.wolfram.com/groups/-/m/t/3217387
| Iscalc: An Interactive Symbolic Computation Framework (System Description) | SpringerLink |
https://link.springer.com/chapter/10.1007/978-3-031-38499-8_33
https://4chan-science.fandom.com/wiki/Physics_Textbook_Recommendations
francois.boulier/DifferentialAlgebra: Differential Algebra is an algebraic theory for handling systems of polynomial (hence nonlinear) differential equations with respect to finitely many differentiations (it thus handles ODE and PDE). The main tool provided by this project is a differential elimination method which permits to simplify such systems. Examples of applications can be found in the gallery directory. - Codeberg.org
https://codeberg.org/francois.boulier/DifferentialAlgebra
| Writing a BIOS bootloader for 64-bit mode from scratch | Hacker News |
https://news.ycombinator.com/item?id=40959742
https://www.sciencedirect.com/science/article/pii/S2352711018302152
Practically surreal: Surreal arithmetic in Julia
https://project-coco.uibk.ac.at/ARI/index.php
Confluence competition
Scheme books
https://erkin.party/scheme/bibliography/
2024-05
https://project-coco.uibk.ac.at/ARI/index.php
Confluence competition
Scheme books
https://erkin.party/scheme/bibliography/
| Ask HN: Where are the good resources for learning audio processing? | Hacker News |
https://news.ycombinator.com/item?id=40892812
| How to implement a hash table in C (2021) | Hacker News |
https://news.ycombinator.com/item?id=40887806
https://arxiv.org/pdf/2005.11644
Sumbolic minikanren for python brandon willard
http://minikanren.org/workshop/2020/minikanren-2020-paper11.pdf
Doug Lenat’s source code for AM and EURISKO (+Traveller?) found in public archives
https://white-flame.com/am-eurisko.html
CS252R: Programming Languages + Artificial Intelligence (Fall 2020)
https://pl-ai-seminar.seas.harvard.edu/home
| The algorithmization of counterfactuals | CS252R: Programming Languages + Artificial Intelligence (Fall 2020) |
https://pl-ai-seminar.seas.harvard.edu/publications/algorithmization-counterfactuals
Andorra I: a parallel Prolog system that transparently exploits both And-and or-parallelism: ACM SIGPLAN Notices: Vol 26, No 7
https://dl.acm.org/doi/10.1145/109626.109635
| Microcontroller Exploits | No Starch Press |
https://nostarch.com/microcontroller-exploits
https://haslab.github.io/MFES/2122/CBMCexamples-handout.pdf
| History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie! | SpringerLink |
https://link.springer.com/chapter/10.1007/978-3-540-32254-2_12
blog :: Brent -> [String] - Products with unordered n-tuples
https://byorgey.github.io/blog/posts/2024/06/25/unordered-n-tuple-product.html
xDSL
Devito: a scalable and portable stencil DSL and compiler
https://www.devitoproject.org/
The Firedrake project — Firedrake 0+unknown documentation
https://www.firedrakeproject.org/
NAS Parallel Benchmarks
https://www.nas.nasa.gov/software/npb.html
SpEQ: Translation of Sparse Codes using Equivalences
https://zenodo.org/records/10963236
[2403.06707] Deriving Dependently-Typed OOP from First Principles – Extended Version with Additional Appendices
https://arxiv.org/abs/2403.06707
Control structures
https://xavierleroy.org/CdF/2023-2024/index.html
https://pl.cs.princeton.edu/generals/slides/dh7120.pdf
He egraph
Functional Data Structures and Algorithms. A Proof Assistant Approach
https://functional-algorithms-verified.org/
https://www.phil.cmu.edu/projects/apros/pdf/normal_natural_deduction.pdf
Soeg byrnes interfaclation. Natural deduction normal forms
https://users.cs.northwestern.edu/~robby/pubs/papers/fb-tr2006-01.pdf
Higher order contracts
https://ceur-ws.org/Vol-2162/paper-03.pdf
Efficient translation of sequent to natural gebner
https://archive.model.in.tum.de/um/bibdb/kiefer/dlt07.pdf
Newton method in semirigns
| Symbolic Boolean derivatives for efficiently solving extended regular expression constraints | Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation |
https://dl.acm.org/doi/abs/10.1145/3453483.3454066
https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette/sqj2013-relational.pdf
Relational analysis of cojnductive predicates blanchette nitpick
foundations - Construction of inductive types “the hard way” - Proof Assistants Stack Exchange
A Syntactic Approach to Type Soundness - ScienceDirect
https://www.sciencedirect.com/science/article/pii/S0890540184710935?ref=cra_js_challenge&fr=RR-1
| Nelson Oppen combination as a rewrite theory | IDEALS |
https://www.ideals.illinois.edu/items/107698
https://arxiv.org/pdf/2209.12592
Compressed combinatory proof structures
analysis - What are the consequences if Axiom of Infinity is negated? - Mathematics Stack Exchange
| Taming floating-point sums | Hacker News |
https://news.ycombinator.com/item?id=40477604
Infinitary term graph rewriting
https://arxiv.org/pdf/2403.04017
learning guided auotmated reasoning a survey
(PDF) Proof-planning Non-standard Analysis
https://www.researchgate.net/publication/2905525_Proof-planning_Non-standard_Analysis
| Continued Fractions Without Tears | Mathematical Association of America |
https://maa.org/programs/maa-awards/writing-awards/continued-fractions-without-tears
| F* – A Proof-Oriented Programming Language | Hacker News |
https://news.ycombinator.com/item?id=40377685
| Some notes on Rust, mutable aliasing and formal verification | Hacker News |
https://news.ycombinator.com/item?id=40375341
Ordinals.CumulativeHierarchy
https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.CumulativeHierarchy.html
Agda ordinals
Hereditary multisets
Multiset theory
[1610.08027] Multisets in Type Theory
https://arxiv.org/abs/1610.08027
https://people.math.harvard.edu/~knill/
Publications of the Programming Systems Lab
https://www.ps.uni-saarland.de/Publications/list/all.html
Poleiro, the Coq blog - An introduction to combinatorial game theory
https://poleiro.info/posts/2013-09-08-an-introduction-to-combinatorial-game-theory.html
https://www.bc.edu/content/dam/bc1/schools/mcas/cs/pdf/honors-thesis/sample5.pdf
Qbf for games
| Tour of CLIPS (2022) | Hacker News |
https://news.ycombinator.com/item?id=40201729
PolyBench/C – Homepage of Louis-Noël Pouchet
https://web.cs.ucla.edu/~pouchet/software/polybench/
| Compactness. Part 1: Degrees of freedom | Bubbles Bad; Ripples Good |
https://williewong.wordpress.com/2010/03/18/compactness-part-1-degrees-of-freedom/
https://quarto.org/docs/books/
https://en.wikipedia.org/wiki/Deep_learning_super_sampling
https://algebraicjulia.github.io/Kittenlab.jl/
https://events.model.in.tum.de/mod23/blanchette/Lecture3-Lambda-Superposition.pdf
Superposition black egtte
| Legendre Transform, Better Explained (2017) | Hacker News |
https://news.ycombinator.com/item?id=39916165
https://jasongross.github.io/lob-paper/nightly/lob.pdf
http://users.dimi.uniud.it/~agostino.dovier/PAPERS/tesi_1mar96.pdf
Compitable set in logic programming thesis
How did cantor discovoer set theory and topology
https://www.ias.ac.in/article/fulltext/reso/019/11/0977-0999
| Uniqueness of trigonometric series and descriptive set theory, 1870–1985 | Archive for History of Exact Sciences |
https://link.springer.com/article/10.1007/BF01886630
http://joerg.endrullis.de//assets/papers/rewriting-braids-2019.pdf
| The Mechanics of Proof | Hacker News |
https://news.ycombinator.com/item?id=39760379
Photonic Crystals: Molding the Flow of Light
http://ab-initio.mit.edu/book/
| Mathematics and Computation | The Dialectica interpertation in Coq |
https://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/
https://dialnet.unirioja.es/descarga/articulo/3216575.pdf
Kenzo acl2
https://backend.orbit.dtu.dk/ws/portalfiles/portal/163079794/phd493_Schlichtkrull_A.pdf
Metatheory in isabelle
Implementing nominal unficiation
Impelenting nominal unification
Ajj dick knuth bendix
Ajj dick
Knuth bendix
| Linux/ELF .eh_frame from the bottom up | Hacker News |
https://news.ycombinator.com/item?id=39367243
| Magika: AI powered fast and efficient file type identification | Hacker News |
https://news.ycombinator.com/item?id=39391688
Holistic Evaluation of Language Models (HELM)
https://crfm.stanford.edu/helm/lite/latest/
Simon Willison on promptinjection
https://simonwillison.net/tags/promptinjection/
PULP FAQs
https://blog.regehr.org/archives/213
https://arxiv.org/pdf/1807.03777.pdf
Welcome to GROMACS — GROMACS webpage https://www.gromacs.org documentation
| You can run Rust code in a Jupyter notebook | Hacker News |
https://news.ycombinator.com/item?id=34380914
| Scriptisto: “Shebang interpreter” that enables writing scripts in compiled langs | Hacker News |
https://news.ycombinator.com/item?id=39272890
https://www.cs.princeton.edu/~appel/papers/bringing-order.pdf
Bringing order separation logic
| Advanced binary fuzzing using AFL++-QEMU and libprotobuf: a practical case of grammar-aware in-memory persistent fuzzing | Blogpost about optimizing binary-only fuzzing with AFL++ |
https://airbus-seclab.github.io/AFLplusplus-blogpost/
Babylon.js: Powerful, Beautiful, Simple, Open - Web-Based 3D At Its Best
Presentations/PSConfEU2023/TuningLinuxforPerformance/demo.sh at master · nocentino/Presentations · GitHub
| Power Management | System Analysis and Tuning Guide | openSUSE Leap 42.2 |
Initial ramdisk - Wikipedia
https://en.m.wikipedia.org/wiki/Initial_ramdisk
drivers - Touchpad causes huge amount of interrupts and high power usage - Ask Ubuntu
Interrupt storm - Wikipedia
https://en.wikipedia.org/wiki/Interrupt_storm
Kernel parameters - ArchWiki
https://wiki.archlinux.org/title/kernel_parameters
https://linux-kernel-labs.github.io/refs/heads/master/index.html
https://github.com/stephenrkell/liballocs/
https://news.ycombinator.com/item?id=39066741
| Two handy GDB breakpoint tricks | Hacker News |
https://news.ycombinator.com/item?id=39170901
| Ask HN: Best open source and/or free EDA tooling | Hacker News |
https://news.ycombinator.com/item?id=39163522
| —-libcurl | Hacker News |
https://news.ycombinator.com/item?id=39175873
All my favorite tracing tools: eBPF, QEMU, Perfetto, new ones I built and more - Tristan Hume
https://thume.ca/2023/12/02/tracing-methods/
| openEMS | openEMS is a free and open electromagnetic field solver using the FDTD method. |
GitHub - johnthagen/min-sized-rust: 🦀 How to minimize Rust binary size 📦
https://github.com/johnthagen/min-sized-rust
https://people.cs.rutgers.edu/~sn349/papers/agni-cav2023.pdf
| AlphaGeometry: An Olympiad-level AI system for geometry | Hacker News |
https://news.ycombinator.com/item?id=39029801
| K/simple: a tiny K interpreter for educational purposes by Arthur Whitney | Hacker News |
https://news.ycombinator.com/item?id=39026551
The many faces of LLVM PGO and FDO
https://aaupov.github.io/blog/2023/07/09/pgo
https://news.ycombinator.com/item?id=38863339
https://bernsteinbear.com//blog/typed-c-extensions/
https://github.com/Microsoft/llvm-mctoll
so good
https://github.com/marcpaq/b1fipl?tab=readme-ov-file
| Modal Satisfiability via SMT Solving | SpringerLink |
https://link.springer.com/chapter/10.1007/978-3-319-15545-6_5
| Python 3.13 Gets a JIT | Hacker News |
https://news.ycombinator.com/item?id=38923741
| k on pdp11 | Hacker News |
https://news.ycombinator.com/item?id=38912406
| Dealing with Weird ELF Libraries | Hacker News |
https://news.ycombinator.com/item?id=38847750
leino.science, home of K. Rustan M. Leino
https://leino.science/dafny-power-user/
Well founded in dadny, calc in dafny
Amaranth HDL documentation — Amaranth HDL toolchain 0.4.1.dev22 documentation
https://amaranth-lang.org/docs/amaranth/latest/cover.html#
| SIMD in Pure Python | Hacker News |
https://news.ycombinator.com/item?id=38874885
GitHub - kparc/pf: tiny printf(3) for bare metal
https://github.com/rapid7/mettle
user land exec for metasploit
lambda calculus - What are pertinent references to cite on Scott domains? - Theoretical Computer Science Stack Exchange
https://www.cis.upenn.edu/~euisuny/paper/perr.pdf
https://www.cs.cmu.edu/~fox/pcc.html
The Fox Project Proof-Carrying Code