Google Keep
Export Method: Highlight, select copy to google doc.
2024-12
https://williamjbowman.com/tmp/nbe-four-ways/
https://news.ycombinator.com/item?id=42440767
| CRIU, a project to implement checkpoint/restore functionality for Linux | Hacker News |
https://news.ycombinator.com/item?id=40751468
| All you need is call/cc (2013) | Hacker News |
https://news.ycombinator.com/item?id=28287312
https://www.cl.cam.ac.uk/teaching/2324/R277/handout-delimited-continuations.pdf
How would set theory research be affected by using ETCS instead of ZFC? - MathOverflow
| Spherical Harmonics | Hacker News |
https://news.ycombinator.com/item?id=42468554
https://people.mpi-sws.org/~dreyer/papers/pedrot-exceptional/paper.pdf
Failure is not an option
[1602.04530] The Independence of Markov’s Principle in Type Theory
https://arxiv.org/abs/1602.04530
[2210.05346] Stateful Realizers for Nonstandard Analysis
https://arxiv.org/abs/2210.05346
https://dspace.library.uu.nl/bitstream/handle/1874/1945/1131.pdf
History of realizability
https://www.irif.fr/~krivine/articles/Luminy04.pdf
Krivine realizability
| Genesis – a generative physics engine for general-purpose robotics | Hacker News |
https://news.ycombinator.com/item?id=42457213
https://arxiv.org/pdf/1810.08380
Computability in lean carneiro
| Modelica | Hacker News |
https://news.ycombinator.com/item?id=42431186
Quantum hands on experiments
| Physics Experiments with Arduino and Smartphones | SpringerLink |
https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette/lambda_free_kbo_conf.pdf
Lambda free kbo
https://ceur-ws.org/Vol-2271/paper1.pdf
Tarau ljt
TypesAndProofs/third_party/dyckhoff_orig.pro at master · ptarau/TypesAndProofs · GitHub
https://github.com/ptarau/TypesAndProofs/blob/master/third_party/dyckhoff_orig.pro
http://www.cs.cmu.edu/~fp/courses/15317-f08/cmuonly/dyckhoff92.pdf
Ljt dyckhoff 92
https://math.stanford.edu/~ralph/fiber.pdf
[2412.03124] Explicit Weakening
https://arxiv.org/abs/2412.03124
https://kth.diva-portal.org/smash/get/diva2:858615/FULLTEXT01.pdf
Realizability in coq thesis
lo.logic - How exactly are realizability and the Curry-Howard correspondence related? - MathOverflow
https://www2.mathematik.tu-darmstadt.de/~streicher/REAL/REAL.pdf
Realizability streicher
https://dl.acm.org/doi/pdf/10.1145/125826.125848
Omega test
https://www.cl.cam.ac.uk/~nk480/bidir.pdf
Complete easy bidrectional
Automated reasoning techniques as proof-search in sequent calculus - Inria - Institut national de recherche en sciences et technologies du numérique
https://inria.hal.science/hal-00939124/
https://arxiv.org/pdf/1903.00982
https://dl.acm.org/doi/fullHtml/10.1145/3443420
arash thesis
sat - Ways to think formally about Satisfiability Modulo Theories - Theoretical Computer Science Stack Exchange
| The Hoare Cube | Hacker News |
https://news.ycombinator.com/item?id=42320180
https://github.com/abarnert/levicivita
| Derivative at a Discontinuity | Hacker News |
https://news.ycombinator.com/item?id=42312376
[1407.2650v3] Logic and linear algebra: an introduction
https://arxiv.org/abs/1407.2650
| Welcome Page | Advanced Lab |
http://experimentationlab.berkeley.edu/node/2
| Reading Recommendations | Annoying Precision |
https://qchu.wordpress.com/reading-recommendations/
| A categorical unification algorithm | SpringerLink |
https://link.springer.com/chapter/10.1007/3-540-17162-2_139
Circuit Idea - Wikibooks, open books for an open world
https://en.wikibooks.org/wiki/Circuit_Idea
Circuit Idea - Wikibooks, open books for an open world
https://en.wikibooks.org/wiki/Circuit_Idea
https://arxiv.org/pdf/1211.6463
Elecrtromotive force guide
| Category Theory in Programming | Hacker News |
https://news.ycombinator.com/item?id=42291141
The Color of Noise
https://caseymuratori.com/blog_0010
Pernosco
https://news.ycombinator.com/item?id=42260030
https://jesper.cx/files/building-a-cbc-type-checker.pdf
https://cdn.prod.website-files.com/65c089cfdfce11a0392e5c42/67469a196f855821380fffa4_GR-2024.pdf
General relativity baumann notes
| You can use C-Reduce for any language | Hacker News |
https://news.ycombinator.com/item?id=42258103
https://www.danielgratzer.com/papers/type-theory-book.pdf
https://arxiv.org/pdf/2304.01315
Empirical diesgn in reinforcment learning
satisfiiability modulo rewriting
https://github.com/NikolajBjorner/ShonanArtOfSAT/blob/main/AkihisaYamada-slides.pdf
https://www21.in.tum.de/students/set_theory_partial_functions/index.html
https://page.mi.fu-berlin.de/cbenzmueller/papers/C57.pdf
automating free logic in hol benzmuller scott
https://gebner.org/pdfs/2018-08-14_lktond.pdf
Lk ndconversion
https://link.springer.com/chapter/10.1007/978-3-319-23506-6_12
https://www.tcs.ifi.lmu.de/lehre/ws-2024-25/atp/paper.pdf
https://core.ac.uk/download/303691264.pdf
https://people.mpi-inf.mpg.de/~mfleury/paper/Weidenback_Book_CDCL.pdf
https://imrclab.github.io/teaching/motion-planning
sagemath references
https://doc.sagemath.org/html/en/reference/references/index.html
https://arxiv.org/abs/2212.00831
https://www.cs.cmu.edu/~15414/s22/lectures/13-resolution.pdf
Uwe Waldmann - Automated Reasoning - Suggested Readings
https://rg1-teaching.mpi-inf.mpg.de/autrea-ws23/readings.html
https://arxiv.org/pdf/2411.07211
Exo 2
https://www2.mathematik.tu-darmstadt.de/%7Ekohlenbach/novikov.pdf
Proof mining kohlenbeck oliva
| Model Predictive Control in the Browser with WebAssembly | Hacker News |
https://news.ycombinator.com/item?id=41992851
[2109.00110] MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
https://arxiv.org/abs/2109.00110
| Designing a Home Radio Telescope for 21 Cm Emission | Hacker News |
https://news.ycombinator.com/item?id=42044494
Termination of polynomial interp
| Breaking CityHash64, MurmurHash2/3, wyhash, and more… | orlp.net |
https://orlp.net/blog/breaking-hash-functions/
https://www.lrde.epita.fr/wiki/Painless
PolyBoRi - Polynomials over Boolean Rings: Overview
https://polybori.sourceforge.net/
https://www.forth.org/fd/contents.html
https://arxiv.org/abs/2404.18249
https://rg1-teaching.mpi-inf.mpg.de/autrea-ws21/notes-3d.pdf
Ordered resolution with selection
https://dl.acm.org/doi/pdf/10.1145/321420.321428
Slagle resolution 1967
Team VLSI - Learn and grow together!
A primer on code generation in Cranelift by Benjamin Bouvier
https://bouvier.cc/cranelift-codegen-primer/
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-705.pdf
Vsdg
https://gcc-python-plugin.readthedocs.io/en/latest/working-with-c.html
gcc python
NandGame - Build a computer from scratch.
https://www.inf.ed.ac.uk/publications/online/0242.pdf
Geometry explorer full angle
http://www.mmrc.iss.ac.cn/~xgao/paper/jgex.pdf
Java geometry expert
wsolve
http://www.mmrc.iss.ac.cn/~dwang/wsolve.html
[2312.07263] A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
https://arxiv.org/abs/2312.07263
MFEM - Finite Element Discretization Library
Project PHYSNET 27Sep2015
https://news.ycombinator.com/item?id=41922081
https://news.ycombinator.com/item?id=41926669
More Coupled Oscillators
https://lewinb.net/posts/09_more_coupled_oscillators/
https://www.math.unl.edu/~jkettinger2/thurston.pdf
Geoemtry of 3 manifolds thurston
| Pygfx | Hacker News |
https://news.ycombinator.com/item?id=41919246
Thermometer continuations, part 2 - Calvin Woo’s blog
https://calwoo.github.io/posts/2020-02-15-thermometer_p2.html
Computing optimal hypertree decompositions with SAT - ScienceDirect
https://www.sciencedirect.com/science/article/pii/S0004370223001613
Juho Hirvonen and Jukka Suomela: Distributed Algorithms 2020
https://jukkasuomela.fi/da2020/
http://cgm.cs.mcgill.ca/~breed/2015COMP362/canonicallabellingpaper.pdf
Mcclay canonical graph isomorphism
[1301.1493] Practical graph isomorphism, II
https://arxiv.org/abs/1301.1493
https://www.damtp.cam.ac.uk/user/gold/pdfs/purcell.pdf
Life at low reynolds number
https://www.ijcai.org/Proceedings/85-1/Papers/038.pdf
synthesis by completion dershowitz
https://web.mit.edu/shawest/Public/Papers/cat_gauge_theory.PDF
Gauge theory of cats
| Riemann Tensor Polynomial Canonicalization by Graph Algebra Extension | Proceedings of the 2017 ACM International Symposium on Symbolic and Algebraic Computation |
https://dl.acm.org/doi/abs/10.1145/3087604.3087625
https://www.cs.tau.ac.il/~nachumd/papers/CompletionApplications.pdf
dershowitz completion. AC. inductionless induction. first order theorem proving
https://news.ycombinator.com/item?id=41845884
Goal driven kb
https://rigtriv.wordpress.com/ag-from-the-beginning/
algebraic geometry
https://news.ycombinator.com/item?id=41853780
| The problem of reasoning from inequalities | Journal of Automated Reasoning |
https://link.springer.com/article/10.1007/BF02341857
| Automated Reasoning in Kleene Algebra | SpringerLink |
https://link.springer.com/chapter/10.1007/978-3-540-73595-3_19
| Automated Theorem Proving Practice with Null Geometric Algebra | Journal of Systems Science and Complexity |
https://link.springer.com/article/10.1007/s11424-019-8354-2
| Finding Proofs in Tarskian Geometry | Journal of Automated Reasoning |
https://link.springer.com/article/10.1007/s10817-016-9392-2
https://dspace.mit.edu/bitstream/handle/1721.1/149121/MIT-LCS-TM-312.pdf?sequence=1&isAllowed=y
Hierarchical inequality reasoning bounder
Analytica. Mathematica as a theorem prover
| Use Prolog to improve LLM’s reasoning | Hacker News |
https://news.ycombinator.com/item?id=41831735
https://web.engr.oregonstate.edu/~huanlian/papers/knuth77.pdf
Knuth extraction
A liveness example in TLA+ – Surfing Complexity
https://surfingcomplexity.blog/2024/10/16/a-liveness-example-in-tla/
| The backchase revisited | The VLDB Journal — The International Journal on Very Large Data Bases |
https://dl.acm.org/doi/10.1007/s00778-013-0333-y
| The backchase revisited | The VLDB Journal — The International Journal on Very Large Data Bases |
https://dl.acm.org/doi/10.1007/s00778-013-0333-y
Not your usual #science #blog – @ernestyalumni
https://ernestyalumni.wordpress.com/
https://noamz.org/talks/logpolpro.pdf
Polarity zeilberger
Combinatorics Videos (Igor Pak’s collection)
https://www.math.ucla.edu/~pak/lectures/Math-Videos/comb-videos.htm
| Monte Carlo Hypothesis Tests versus Traditional Parametric Tests | by MCMC Addict | Medium |
https://www.clear.rice.edu/comp512/Lectures/Papers/1971-allen-catalog.pdf
Frances allen optimizing compiler
https://news.ycombinator.com/item?id=41808013
https://download.tek.com/document/LowLevelHandbook_7Ed.pdf
Low level measurmeent handbook
https://news.ycombinator.com/item?id=41808696
The Measurement, Instrumentation and Sensors Handbook (Electrical Engineering Handbook): Webster, John G.: 9780849383472: Amazon.com: Books
https://www.amazon.com/Measurement-Instrumentation-Handbook-Electrical-Engineering/dp/0849383471
| Game Programming in Prolog | Hacker News |
https://news.ycombinator.com/item?id=41800764
https://api.newton.ac.uk/website/v0/seminars/44425/presentation-files/1642 ACL2 x86 bootloading
http://lya.fciencias.unam.mx/favio/publ/cocalculus.pdf
coinductive calculus escardo pavlovic
https://arxiv.org/abs/2410.00065
https://dl.acm.org/doi/abs/10.1145/3589246.3595372
https://dl.acm.org/doi/10.1145/3528416.3530249
https://inria.hal.science/file/index/docid/77199/filename/RR-3400.pdf
Theorem proving modulo
https://arxiv.org/pdf/math/0310194
Sturmfels linear programming and grobner
Patterns of data flow in words
https://okmij.org/ftp/Computation/ARPL.html
Optimizing AXPY
https://okmij.org/ftp/meta-programming/tutorial/daxpy.html#preview
pypy/rpython/jit/metainterp/ruleopt/README.md at jit-opt-dsl · pypy/pypy · GitHub
https://github.com/pypy/pypy/blob/jit-opt-dsl/rpython/jit/metainterp/ruleopt/README.md
Pypy jit rule opt dsl
| Futexes in TLA+ | Hacker News |
https://news.ycombinator.com/item?id=41780409
https://arxiv.org/pdf/2407.12794
Learned egraph scheduling
| Show HN: Compiling C in the browser using WebAssembly | Hacker News |
https://news.ycombinator.com/item?id=41767644
| Mathematical Writing Style Guide for Stanford EE 364B [pdf] (2014) | Hacker News |
https://news.ycombinator.com/item?id=41756286
| Playing with BOLT and Postgres | Hacker News |
https://news.ycombinator.com/item?id=41743464
https://link.springer.com/chapter/10.1007/978-0-387-35498-9_52
soft question - What CS blogs should everyone read? - Theoretical Computer Science Stack Exchange
https://cstheory.stackexchange.com/questions/22191/what-cs-blogs-should-everyone-read
| Assemblage | A dataset (and tool for building) binary executable corpuses. |
https://assemblage-dataset.net/
IRIS
https://iris-programming.github.io/
StarPU
https://starpu.gitlabpages.inria.fr/
Parsec
GRANITE: A Graph Neural Network Model for Basic Block Throughput Estimation
Rev. Mod. Phys. 96, 031002 (2024) - Colloquium: Eigenvector continuation and projection-based emulators
https://link.aps.org/doi/10.1103/RevModPhys.96.031002
Optimizing Vector Instruction Selection for Digital Signal Processing
https://dspace.mit.edu/handle/1721.1/144935?show=full
MUltseq v2.0-2-gf2ad99b
Is there a proof assistant for Peano Arithmetic? - Proof Assistants Stack Exchange
| FFT-based ocean-wave rendering, implemented in Godot | Hacker News |
https://news.ycombinator.com/item?id=41678412
| Python for Inversive and Hyperbolic Geometry | Hacker News |
https://news.ycombinator.com/item?id=41675029
Cello • High Level C
| Learning to optimize halide with tree search and random programs | ACM Transactions on Graphics |
https://dl.acm.org/doi/10.1145/3306346.3322967
awesome-tensor-compilers/README.md at master · merrymercy/awesome-tensor-compilers
https://github.com/merrymercy/awesome-tensor-compilers/blob/master/README.md
[2302.11405] ML-driven Hardware Cost Model for MLIR
https://arxiv.org/abs/2302.11405
https://cnandi.com/docs/oopsla23-cr.pdf
https://inst.eecs.berkeley.edu/~cs294-260/sp24/papers/verifying-halide-trs.pdf
[2409.11424] LlamaF: An Efficient Llama2 Architecture Accelerator on Embedded FPGAs
https://arxiv.org/abs/2409.11424
| Announcing an automatic theorem proving project | Gowers’s Weblog |
https://gowers.wordpress.com/2022/04/28/announcing-an-automatic-theorem-proving-project/
Kernighan–Lin algorithm - Wikipedia
https://en.wikipedia.org/wiki/Kernighan%E2%80%93Lin_algorithm
https://news.ycombinator.com/item?id=41579268
https://www.answer.ai/posts/2024-09-12-gpupuzzles.html
diy torch
| The Visualization of Differential Forms (2021) | Hacker News |
https://news.ycombinator.com/item?id=41609744
https://www.cse.chalmers.se/research/group/logic/book/book.pdf
Thompson programming in martin lof
https://rootjalex.github.io/publications/asplos2023-pitchfork.pdf
https://arxiv.org/html/2306.13002v3
https://www.cs.utexas.edu/~moore/acl2/manuals/latest/index.html?topic=ACL2____DEFDATA
Acl2s has dependent types?
Edmonds’ algorithm - Wikipedia
https://en.m.wikipedia.org/wiki/Edmonds%27_algorithm
Minimum spanning tree on directed graphs
OpenGL Sphere
https://www.songho.ca/opengl/gl_sphere.html
https://www21.in.tum.de/~nipkow/pubs/jar10.pdf
Quantifier elimination nipkow
Star-Tracker Algorithm for Smartphones and Commercial Micro-Drones - PMC
https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7070887/
| Guidance Navigation & Control | NESC Academy Online |
https://nescacademy.nasa.gov/catalogs/gnandc
| LiteRT overview | Google AI Edge | Google AI for Developers |
https://ai.google.dev/edge/litert
https://fse.studenttheses.ub.rug.nl/11323/1/Masterscriptie.pdf
Grobner and graver in mixed integer programming thesis
https://github.com/connorferster/handcalcs?tab=readme-ov-file
https://people.cs.uchicago.edu/~laci/papers/icm18-babai.pdf
Groups graphs algorithms isomorphisms
https://arxiv.org/pdf/2401.15436
Discrete exterior calc non triangle
GAP in Education
https://www.math.colostate.edu/~hulpke/CGT/education.html
Notes on computational group theory
https://github.com/awslabs/shuttle
https://fmv.jku.at/papers/Kaufmann-IWSBP20.pdf
Integer multiplier circuits verification
Them Birds Men’s Perfect Tee By radiomode - Design By Humans
| Computational group theory, 2 | Peter Cameron’s Blog |
https://cameroncounts.wordpress.com/2014/09/22/computational-group-theory-2/
Security protocol analysis tools
https://people.cispa.io/cas.cremers/tools/index.html
| A Survey of Practical Formal Methods for Security | Formal Aspects of Computing |
https://dl.acm.org/doi/full/10.1145/3522582?trk=public_post_comment-text
[WSRP24] Monoids, string-rewriting, confluence, and the Knuth-Bendix Algorithm - Online Technical Discussion Groups—Wolfram Community
https://community.wolfram.com/groups/-/m/t/3217387
https://people.cs.nott.ac.uk/pszgmh/ccc.pdf
Calculate correct compilers
Red Pitaya - Swiss Army Knife For Engineers
torch.nn.Conv2d on FPGA through MLIR and Xilinx Vitis HLS – Максим Левентал – PhD student from somewhere
https://makslevental.github.io/torch-mlir-fpga/
Simulate Electronic Circuit using Python and the Ngspice / Xyce Simulators — PySpice 1.4.2 documentation
https://pyspice.fabrice-salvaire.fr/releases/v1.4/
William Meng
https://williammeng.com/rtl-ultrasound.html
EEVblog – No Script, No Fear, All Opinion
Understanding Analytic Signal and Hilbert Transform - GaussianWaves
https://www.gaussianwaves.com/2017/04/analytic-signal-hilbert-transform-and-fft/
https://vimeo.com/showcase/5271198
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