Google Keep
Export Method: Highlight, select copy to google doc.
2025-04
[1902.08848] Algebraic Type Theory and Universe Hierarchies
https://arxiv.org/abs/1902.08848
Second order gat
[2211.07487] External univalence for second-order generalized algebraic theories
https://arxiv.org/abs/2211.07487
| A refinement type by any other name | weaselhat |
https://www.weaselhat.com/post-531.html
Type universes without ac
[2410.11566] Attitude Estimation via Matrix Fisher Distributions on SO(3) Using Non-Unit Vector Measurements
https://arxiv.org/abs/2410.11566
| Show HN: Torque – A lightweight meta-assembler for any processor | Hacker News |
https://news.ycombinator.com/item?id=43698801
| Designing a low-cost high-performance 10 MHz – 15 GHz vector network analyzer | Hacker News |
https://news.ycombinator.com/item?id=43696798
| What the hell is a target triple? | Hacker News |
https://news.ycombinator.com/item?id=43696756
| Algebraic Semantics for Machine Knitting | Lobsters |
https://lobste.rs/s/koauiz/algebraic_semantics_for_machine
https://noamz.org/oplss16/refinements-notes.pdf
dg.differential geometry - Who first defined vector fields as derivations? - MathOverflow
https://mathoverflow.net/questions/491043/who-first-defined-vector-fields-as-derivations
| Coalgebraically Thinking | The n-Category Café |
https://golem.ph.utexas.edu/category/2008/11/coalgebraically_thinking.html
midpoint algebra in nLab
https://ncatlab.org/nlab/show/midpoint+algebra
https://matryoshka-project.github.io/pubs/vukmirovic_msc_thesis.pdf
| Differential term-orders | Proceedings of the 1993 international symposium on Symbolic and algebraic computation |
https://dl.acm.org/doi/10.1145/164081.164138
https://arxiv.org/abs/2504.05577
https://www.carloangiuli.com/courses/b619-sp24/notes.pdf
Principles of depdent type thwory
https://martinescardo.github.io/.talks/map2011/index.html
categorical computable real talks escardo
OpenRocket Simulator
https://www.sciencedirect.com/science/article/abs/pii/S0001870824001919
| How to not build a two stage model rocket | Hacker News |
https://news.ycombinator.com/item?id=43669981
https://homepages.math.uic.edu/~marker/Banff/AMS_Baltimore.pdf
https://eprints.illc.uva.nl/id/eprint/1769/1/wehr.pdf
czf interpretation
https://arxiv.org/pdf/2411.07667
Formalization of physics index notation in Lean 4
https://www.sciencedirect.com/science/article/pii/S0167642322001435
Martin Escardo: “Index of selected threads on #…” - Mathstodon
https://mathstodon.xyz/@MartinEscardo/110890155815254064
Hott threads
| My Own Private Binary: An Idiosyncratic Introduction to Linux Kernel Modules | Hacker News |
https://news.ycombinator.com/item?id=43647294
[2504.06239] Canonical for Automated Theorem Proving in Lean
https://arxiv.org/abs/2504.06239
https://arxiv.org/pdf/2504.06239
Canonical dependent type solver
https://blog.yosyshq.com/p/risc-v-formal-verification-framework-extension-for-synopsys-vc-formal/
https://www.jjj.de/fxt/#fxtbook
https://www.sciencedirect.com/science/article/pii/S0304397518307278
https://littleosbook.github.io/
https://www.imandra.ai/code-logician
https://cgi.csc.liv.ac.uk/~frans/OldResearch/dGKBIS/tesseral.html
https://leanprover-community.github.io/mathlib4_docs/references.html
https://news.ycombinator.com/item?id=43593088
| Dynamic Register Allocation on AMD’s RDNA 4 GPU Architecture | Hacker News |
https://news.ycombinator.com/item?id=43595223
https://arxiv.org/pdf/2312.02996
Differential term rewriting
| Rewrite Games | SpringerLink |
https://link.springer.com/chapter/10.1007/3-540-45610-4_11
https://repository.tudelft.nl/file/File_a98b6c93-4017-42c5-bb8f-df68da0d7034
Leansolver monte carlo proof search
[2504.01847] Confluence of Conditional Rewriting Modulo
https://arxiv.org/abs/2504.01847
https://akihisayamada.github.io/ADY18.pdf
Probalistic term rewrire systems natt
https://people.eecs.berkeley.edu/~ksen/papers/pmaude.pdf
Probability maude
| String Diagram Rewrite Theory I: Rewriting with Frobenius Structure | Journal of the ACM |
https://dl.acm.org/doi/abs/10.1145/3502719
[1209.3632] Quantum Techniques for Stochastic Mechanics
https://arxiv.org/abs/1209.3632
Probabilistic Programming
https://www.cs.cornell.edu/courses/cs4110/2016fa/lectures/lecture33.html
LazyPPL
https://lazyppl-team.github.io/
[2112.14965] A Braided Lambda Calculus
https://arxiv.org/abs/2112.14965
http://dcernst.github.io/teaching/mat411f16/materials/
| Cayley graphs and the geometry of groups | What’s new |
https://terrytao.wordpress.com/2010/07/10/cayley-graphs-and-the-geometry-of-groups/
Van Kampen diagram - Wikipedia
https://en.wikipedia.org/wiki/Van_Kampen_diagram
| Interferometric single-shot parity measurement in InAs–Al hybrid devices | Nature |
https://www.nature.com/articles/s41586-024-08445-2
| Towards fearless SIMD, 7 years later | Hacker News |
https://news.ycombinator.com/item?id=43519823
https://news.ycombinator.com/item?id=43160779
https://news.ycombinator.com/item?id=43472143
https://ncatlab.org/nlab/show/Tietze+transformation#tietzes_theorem
| Practical SDR | No Starch Press |
https://nostarch.com/practical-sdr
https://www.cse.chalmers.se/~abela/talkCHITCHAT06.pdf
Nbe. Values should be views
Reflection principle - Wikipedia
https://en.m.wikipedia.org/wiki/Reflection_principle
| The Prospero Challenge | Hacker News |
https://news.ycombinator.com/item?id=43458780
| A proof checker meant for education | Hacker News |
https://news.ycombinator.com/item?id=43434503
Book recommendations for network programming : r/golang
https://www.reddit.com/r/golang/comments/v74ji8/book_recommendations_for_network_programming/
https://www.cs.tau.ac.il/~nachum/papers/ProofTheoretic.pdf
Proof theoretic technqiues for term rewriting systems
Kirchener equational. Nice inductionless induction section
https://en.wikipedia.org/wiki/Calculus_of_moving_surfaces
https://dl.acm.org/doi/10.1145/2465506.2466576
The calculus of moving surfaces (CMS)
| Show HN: Torch Lens Maker – Differentiable Geometric Optics in PyTorch | Hacker News |
https://news.ycombinator.com/item?id=43435438
Radio Builder – Home of the RADIO LAB
[2412.05265] Reinforcement Learning: An Overview
https://arxiv.org/abs/2412.05265
| The Inverse Method for the Logic of Bunched Implications | SpringerLink |
https://link.springer.com/chapter/10.1007/978-3-540-32275-7_31
Light’s associativity test - Wikipedia
https://en.m.wikipedia.org/wiki/Light%27s_associativity_test
| DialEgg: Dialect-Agnostic MLIR Optimizer using Equality Saturation with Egglog | Proceedings of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization |
https://dl.acm.org/doi/10.1145/3696443.3708957
https://easychair.org/publications/paper/8jNL/open
Embedding i tuitionistici nto classical
http://www.sontaglab.org/FTPDIR/sontag_mathematical_control_theory_springer98.pdf
Sontag mathematical control theory
Kalman Filter Explained Simply - The Kalman Filter
https://thekalmanfilter.com/kalman-filter-explained-simply/
https://www.bc.edu/content/dam/bc1/schools/mcas/cs/pdf/honors-thesis/sample5.pdf
Solving games qbf solvers
| A Guide to Undefined Behavior in C and C++ (2010) | Hacker News |
https://news.ycombinator.com/item?id=43352503
| Stupid Smart Pointers in C | Hacker News |
https://news.ycombinator.com/item?id=43387334
| Home | PrintedLabs |
https://printedlabs.uni-bayreuth.de/en
https://grantjurgensen.com/posts/schroder-berstein-acl2/
| Amateur Telescope Making Main Page | Hacker News |
https://news.ycombinator.com/item?id=43351988
https://iris-project.org/tutorial-pdfs/iris-lecture-notes.pdf
https://gbaz.github.io/slides/pwl-homology-slides.pdf
| Formal Verification of Zero-Downtime Database Migration in PlusCal | Hacker News |
https://news.ycombinator.com/item?id=43306776
| Formal Verification of Zero-Downtime Database Migration in PlusCal | Hacker News |
https://news.ycombinator.com/item?id=43306776
| Software-Defined Radio for Engineers (2018) [pdf] | Hacker News |
https://news.ycombinator.com/item?id=43323071
Towards a Dynabook for verified VM construction - ScienceDirect
https://www.sciencedirect.com/science/article/pii/S2590118424000182
https://ceur-ws.org/Vol-3325/regular2.pdf
Design principles for high performance smalltalk
| Two decades of smalltalk VM development: live VM development through simulation tools | Proceedings of the 10th ACM SIGPLAN International Workshop on Virtual Machines and Intermediate Languages |
https://dl.acm.org/doi/10.1145/3281287.3281295
Flean: Floating point numbers in Lean, mostly done!
https://josephmckinsey.com/flean2.html
Axiomatic Theories of Truth (Stanford Encyclopedia of Philosophy)
https://plato.stanford.edu/entries/truth-axiomatic/
https://wiki.bordeaux.inria.fr/Helene-Kirchner/doku.php?id=start
IMC010: Type Theory and Coq
https://www.cs.ru.nl/~freek/courses/tt-2024/
https://www.sciencedirect.com/science/article/pii/S0888613X24001725
An implementation of nonmonotonic reasoning with c-representations using an SMT solver
https://arxiv.org/pdf/2501.00921
https://github.com/Wilfred/difftastic/wiki/Structural-Diffs
https://arxiv.org/abs/2304.06000
Ground Confluence Prover based on Rewriting Induction - CORE Reader
https://core.ac.uk/reader/62921510
| A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL | Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs |
https://dl.acm.org/doi/10.1145/3293880.3294098
https://www.cs.cmu.edu/~fp/papers/adjoint18b.pdf
Adjoint logic
| Mistral OCR | Hacker News |
https://news.ycombinator.com/item?id=43282905
Hands-On Mathematical Optimization with Python — Companion code for the book “Hands-On Mathematical Optimization with Python”
https://mobook.github.io/MO-book/intro.html
https://www.chargueraud.org/research/2025/overloading/overloading.pdf
Typechecking overloading
How to deepen your understanding of Mizar – Ariadne’s Thread
https://thmprover.wordpress.com/2025/02/22/how-to-deepen-your-understanding-of-mizar/
| An Attempt to Catch Up with JIT Compilers | Hacker News |
https://news.ycombinator.com/item?id=43243109
HomePage:Finite Element Method Magnetics
https://www.femm.info/wiki/HomePage
| Antenna Design Tools | AEM Antennas |
https://aemantennas.com/antenna-design-tools/
Hedgehog (geometry) - Wikipedia
https://en.m.wikipedia.org/wiki/Hedgehog_(geometry)
Home
https://csadams.webspace.durham.ac.uk/
Optics f2f Code Book — Optics f2f Code Book
https://opticsf2f.github.io/Opticsf2f_CodeBook/intro.html
Optics f2f - Paperback - Charles S. Adams, Ifan G. Hughes - Oxford University Press
https://global.oup.com/academic/product/optics-f2f-9780198786795?cc=gb&lang=en&
https://news.ycombinator.com/item?id=43204796
https://fpga-ignite.github.io/
Game Engine Black Book DOOM
https://fabiensanglard.net/gebbdoom/
[2502.19311] Faithful Logic Embeddings in HOL – A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level
https://arxiv.org/abs/2502.19311
[2304.06000] Pointfree topology and constructive mathematics
https://arxiv.org/abs/2304.06000
| A $100 DIY muon tomographer | Hacker News |
https://news.ycombinator.com/item?id=43195525
| The need for memory safety standards | Hacker News |
https://news.ycombinator.com/item?id=43186614
| Geometric Algebra | Hacker News |
https://news.ycombinator.com/item?id=43189703
| Calculus Without Derivatives | SpringerLink |
https://link.springer.com/book/10.1007/978-1-4614-4538-8
| History of CAD | Hacker News |
https://news.ycombinator.com/item?id=43167865
| Long division verified via Hoare logic | Hacker News |
https://news.ycombinator.com/item?id=43185059
https://gist.github.com/cfbolz/4ad3e137850c17f02348411eb9de2186/revisions
| Low Overhead Allocation Sampling with VMProf in PyPy’s GC | PyPy |
https://www.pypy.org/posts/2025/02/pypy-gc-sampling.html
| Introduction to Stochastic Calculus | Hacker News |
https://news.ycombinator.com/item?id=43160779
| Topological Superconductors | Hacker News |
https://news.ycombinator.com/item?id=43105916
https://news.ycombinator.com/item?id=43140614
| Design of Experiments | JMP |
https://www.jmp.com/en_us/software/capabilities/design-of-experiments.html
| TinyCompiler: A compiler in a week-end | Hacker News |
https://news.ycombinator.com/item?id=43120873
https://github.com/a327ex/blog/issues/15
https://www.vldb.org/pvldb/vol1/1453978.pdf database rewrite rules according to max willsey
https://www.csl.cornell.edu/~zhiruz/pdfs/smoothe-asplos2025.pdf differnetiable egraph extraction
https://arxiv.org/pdf/2404.08106 kestrel relational egraph
KDLP
https://kdlp.underground.software/course/index
https://www.teachspin.com/instruments
https://news.ycombinator.com/item?id=43048073
https://homepage.divms.uiowa.edu/~slonnegr/plf/Book/
| Homemade polarimetric synthetic aperture radar drone | Hacker News |
https://news.ycombinator.com/item?id=43073808
https://github.com/tum-pbs/PhiFlow
| Flea-Scope: $18 Source Available USB Oscilloscope, Logic Analyzer and More [pdf] | Hacker News |
https://news.ycombinator.com/item?id=43068585
| Show HN: Letting LLMs Run a Debugger | Hacker News |
https://news.ycombinator.com/item?id=43023698
https://math.andrej.com/data/synthetic.pdf
First steps in synthetic computability theory
Introduction to Applied Linear Algebra – Vectors, Matrices, and Least Squares
https://web.stanford.edu/~boyd/vmls/
| Jill – a functional programming language for the Nand2Tetris platform | Hacker News |
https://news.ycombinator.com/item?id=43060603
Home · Kenney
Fluidsim documentation — FluidSim 0.8.4 documentation
https://fluidsim.readthedocs.io/en/latest/index.html
| Basis of the Kalman Filter [pdf] | Hacker News |
https://news.ycombinator.com/item?id=43029314
Wokwi - World’s most advanced ESP32 Simulator
| Tiny Pointers | Hacker News |
https://news.ycombinator.com/item?id=43023634
https://www21.in.tum.de/~eberlm/pdfs/algorithms_survey.pdf
Theory Deriv
https://isabelle.in.tum.de/library/HOL/HOL/Deriv.html#Deriv.has_derivative%7Cconst
https://abackus.github.io/research/formalizations.pdf
Formalizatiosn of analysis bishop intuitionsim
https://guillaume.melquiond.fr/doc/14-mscs.pdf
Real analysis formalization
Welcome to bilby’s documentation! — bilby 2.3 documentation
https://lscsoft.docs.ligo.org/bilby/
[2502.03544] Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
https://arxiv.org/abs/2502.03544
Grounded Language Design for Lightweight Diagramming for Formal Methods
https://arxiv.org/html/2412.03310v1
LTL Tutor: Login
https://www.ltl-tutor.xyz/login?next=%2F
successful sat encoding technique
https://news.ycombinator.com/item?id=42918846
llama-vscode - Visual Studio Marketplace
https://marketplace.visualstudio.com/items?itemName=ggml-org.llama-vscode
Development of DSL Compilers for Specialized Processors
https://link.springer.com/article/10.1134/S0361768821070082
https://colab.research.google.com/drive/1jcNgt5SWMHgHjRE8pwekRdFeaED2Ci2y#scrollTo=01PIn9pUGiN2
| copilot-explorer | Hacky repo to see what the Copilot extension sends to the server |
https://thakkarparth007.github.io/copilot-explorer/posts/copilot-internals.html
Power diagram - Wikipedia
https://en.m.wikipedia.org/wiki/Power_diagram
| PCBs, copper pours, ground planes, and you | Hacker News |
https://news.ycombinator.com/item?id=42874885
[2106.03936] Partial Optimal Transport for a Constant-Volume Lagrangian Mesh with Free Boundaries
https://arxiv.org/abs/2106.03936
https://www.lopoukhine.com/winter-school/
https://hvg.ece.concordia.ca/Publications/Thesis/Elif-PhD-Thesis.pdf
Hol light pde
| Anatomy of a Formal Proof | Hacker News |
https://news.ycombinator.com/item?id=42815755
https://www.impan.pl/~kz/truthseminar/Kripke_Outline.pdf
kripke logic towers
https://en.wikipedia.org/wiki/Genetic_programming
https://github.com/FormalizedFormalLogic
https://news.ycombinator.com/item?id=42708682
https://www.inf.ed.ac.uk/teaching/courses/ar/book/book_2010.06.23.pdf
computational modelling of mathematical reasoning - alan bundy
| Physically Based Rendering: From Theory to Implementation | Hacker News |
https://news.ycombinator.com/item?id=42683731
Homepage of Understanding MP3
https://hint.userweb.mwn.de/understanding_mp3/index.html
| Lambda Calculus in 383 Bytes (2022) | Hacker News |
https://news.ycombinator.com/item?id=42679191
https://news.ycombinator.com/item?id=42672246
| The Pi Calculus | The n-Category Café |
https://golem.ph.utexas.edu/category/2009/08/the_pi_calculus.html
https://arxiv.org/abs/math/0411418v2
https://news.ycombinator.com/item?id=42656433
sief natural deduction thesis
https://www.cmu.edu/dietrich/philosophy/docs/tech-reports/74_Sieg.pdf
| Comparing Hobby PCB Vendors | Hacker News |
https://news.ycombinator.com/item?id=35285769
| Choosing an op-amp for your project | Hacker News |
https://news.ycombinator.com/item?id=42590337
| Rohlang3: A point-free, homoiconic, and dependently typed “SK calculus” | Hacker News |
https://news.ycombinator.com/item?id=42581082
| Einsum in Depth | Hacker News |
https://news.ycombinator.com/item?id=42587056
| Musings on Tracing in PyPy | PyPy |
https://pypy.org/posts/2025/01/musings-tracing.html
https://github.com/jsiek/deduce?tab=readme-ov-file
| The Dome (2005) | Hacker News |
https://news.ycombinator.com/item?id=42583688
https://people.mpi-sws.org/~mueck/downloads/paper-csl24.pdf
Forster dominik synthetic computability coq
| Numerical Fuzz: A Type System for Rounding Error Analysis | Proceedings of the ACM on Programming Languages |
https://dl.acm.org/doi/10.1145/3656456
Accurate Polynomial Evaluation in Floating Point - Computational Science Stack Exchange
https://scicomp.stackexchange.com/questions/13023/accurate-polynomial-evaluation-in-floating-point
| Emulating the FMAdd Instruction, Part 1: 32-bit Floats | Hacker News |
https://news.ycombinator.com/item?id=42572770
| 12 Steps to a Fast Multipole Method on GPUs | Pan-American Advanced Studies Institute |
https://www.bu.edu/pasi/courses/12-steps-to-having-a-fast-multipole-method-on-gpus/
algorithm - Recommendations for Fast Multipole Method implementation? - Stack Overflow
| Building Game Prototypes with LÖVE | Hacker News |
https://news.ycombinator.com/item?id=42562175
| Symbolic Reference and Hardware Models in Python | Hacker News |
https://news.ycombinator.com/item?id=42530424
Introduction to PyKX - KX Learning Hub
https://learninghub.kx.com/courses/introduction-to-pykx/
Physics 12c
https://www.preskill.caltech.edu/ph12c/index.html
https://math.andrej.com/wp-content/uploads/2011/01/dialectica.v
| Invariants: Computation and Applications | Hacker News |
https://news.ycombinator.com/item?id=42521718
https://news.ycombinator.com/item?id=42516697
https://martinescardo.github.io/papers/RNC3.pdf
Pcf with reals escardo
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