Google Keep
Export: Highlight, select copy to google doc.
#
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