| | SAT Etudes 2: Toy DPLL (philipzucker.com) |
| 1 point by matt_d 17 days ago | past |
|
| | A Slotted Hash Cons for Alpha Invariance (philipzucker.com) |
| 1 point by g0xA52A2A 3 months ago | past |
|
| | Compositional Datalog on SQL: Relational Algebra of the Environment (philipzucker.com) |
| 47 points by philzook 3 months ago | past | 3 comments |
|
| | Compositional Datalog on SQL: Relational Algebra of the Environment (philipzucker.com) |
| 3 points by Bogdanp 3 months ago | past |
|
| | A Python CLI for Verifying Assembly (philipzucker.com) |
| 1 point by philzook 4 months ago | past |
|
| | A Python CLI for Verifying Assembly (philipzucker.com) |
| 2 points by matt_d 4 months ago | past |
|
| | Semantic Refinement/Dependent Typing for Knuckledragger/SMTLIB Pt 1 (philipzucker.com) |
| 2 points by matt_d 4 months ago | past |
|
| | Verified Assembly 2: Memory, RISC-V, Cuts for Invariants, and Ghost Code (philipzucker.com) |
| 3 points by todsacerdoti 4 months ago | past |
|
| | Semi-Automated Assembly Verification in Python Using Pypcode Semantics (philipzucker.com) |
| 2 points by matt_d 5 months ago | past |
|
| | Inequality Union Finds: Baby Steps to Refinement E-Graphs (philipzucker.com) |
| 1 point by todsacerdoti 5 months ago | past |
|
| | A Python frozenset interpretation of dependent type theory (philipzucker.com) |
| 2 points by fanf2 5 months ago | past |
|
| | Telescopes Are Tries: A Dependent Type Shellac on SQLite (philipzucker.com) |
| 16 points by matt_d 5 months ago | past |
|
| | Brute E-Graphs Modulo Theories 2: Extraction, Proofs, and Context (philipzucker.com) |
| 1 point by matt_d 6 months ago | past |
|
| | A Python Frozenset Interpretation of Dependent Type Theory (philipzucker.com) |
| 5 points by philzook 7 months ago | past |
|
| | "Verified" "Compilation" of "Python" with Knuckledragger, GCC, and Ghidra (philipzucker.com) |
| 2 points by philzook 8 months ago | past |
|
| | A Small Prolog on the Z3 AST (philipzucker.com) |
| 3 points by philzook 8 months ago | past |
|
| | Comparing Two Verilog CPU Implementations Using EBMC (philipzucker.com) |
| 5 points by PaulHoule 10 months ago | past |
|
| | Where are all the rewrite rules? (philipzucker.com) |
| 59 points by todsacerdoti 10 months ago | past | 29 comments |
|
| | Comparing Two Verilog CPU Implementations Using EBMC (philipzucker.com) |
| 10 points by todsacerdoti 10 months ago | past | 1 comment |
|
| | SAT Solver Etudes I (philipzucker.com) |
| 45 points by mathgenius 11 months ago | past | 30 comments |
|
| | Symbolic Execution by Overloading __bool__ (philipzucker.com) |
| 81 points by philzook 12 months ago | past | 10 comments |
|
| | Superposition as a Super Datalog (philipzucker.com) |
| 3 points by iamwil on Dec 2, 2024 | past |
|
| | SQL, Homomorphisms and Constraint Satisfaction Problems (philipzucker.com) |
| 153 points by xlinux on Nov 20, 2024 | past | 19 comments |
|
| | Higher Order Pattern Unification on the Z3py AST (philipzucker.com) |
| 2 points by philzook on Nov 11, 2024 | past |
|
| | Tensors and Graphs: Canonization by Search (philipzucker.com) |
| 1 point by philzook on Nov 4, 2024 | past |
|
| | Don't implement unification by recursion (philipzucker.com) |
| 83 points by mathgenius on Oct 28, 2024 | past | 62 comments |
|
| | Using the C Bounded Model Checker as a TLA+ (philipzucker.com) |
| 3 points by matt_d on Oct 8, 2024 | past |
|
| | Acyclic Egraphs and Smart Constructors (philipzucker.com) |
| 4 points by philzook on Sept 16, 2024 | past |
|
| | String Knuth Bendix (philipzucker.com) |
| 2 points by philzook on Sept 9, 2024 | past |
|
| | Ordinals aren't much worse than Quaternions (philipzucker.com) |
| 62 points by philzook on Aug 22, 2024 | past | 28 comments |
|
|
| More |
