| | SAT Solver Etudes I (philipzucker.com) |
|
45 points by mathgenius 14 days ago | past | 30 comments
|
|
| | Symbolic Execution by Overloading __bool__ (philipzucker.com) |
|
81 points by philzook 29 days ago | past | 10 comments
|
|
| | Superposition as a Super Datalog (philipzucker.com) |
|
3 points by iamwil 50 days ago | past
|
|
| | SQL, Homomorphisms and Constraint Satisfaction Problems (philipzucker.com) |
|
153 points by xlinux 62 days ago | past | 19 comments
|
|
| | Higher Order Pattern Unification on the Z3py AST (philipzucker.com) |
|
2 points by philzook 71 days ago | past
|
|
| | Tensors and Graphs: Canonization by Search (philipzucker.com) |
|
1 point by philzook 78 days ago | past
|
|
| | Don't implement unification by recursion (philipzucker.com) |
|
83 points by mathgenius 85 days ago | past | 62 comments
|
|
| | Using the C Bounded Model Checker as a TLA+ (philipzucker.com) |
|
3 points by matt_d 3 months ago | past
|
|
| | Acyclic Egraphs and Smart Constructors (philipzucker.com) |
|
4 points by philzook 4 months ago | past
|
|
| | String Knuth Bendix (philipzucker.com) |
|
2 points by philzook 4 months ago | past
|
|
| | Ordinals aren't much worse than Quaternions (philipzucker.com) |
|
62 points by philzook 5 months ago | past | 28 comments
|
|
| | Co-Egraphs: Streams, Unification, Pegs, Rational Lambdas (philipzucker.com) |
|
3 points by speckx 5 months ago | past
|
|
| | Knuckledragger, a Semi-Automated Python Proof Assistant (philipzucker.com) |
|
71 points by philzook 5 months ago | past | 24 comments
|
|
| | EGraphs as Ground Completion Talk and Egraphs 2024 Notes (philipzucker.com) |
|
2 points by g0xA52A2A 6 months ago | past
|
|
| | Simple Proofs with Z3Py (2019) (philipzucker.com) |
|
1 point by fanf2 7 months ago | past
|
|
| | Justified SMT 1: The miniKanren inside Z3 (philipzucker.com) |
|
4 points by mpweiher 7 months ago | past
|
|
| | Hashing Modulo Theories (philipzucker.com) |
|
59 points by philzook 8 months ago | past | 3 comments
|
|
| | Reverse Mode Differentiation Is Kind of Like a Lens (philipzucker.com) |
|
1 point by pizza 9 months ago | past
|
|
| | Linear Algebra of Types (2019) (philipzucker.com) |
|
115 points by g0xA52A2A 9 months ago | past | 8 comments
|
|
| | Finite Set Theory in Python (philipzucker.com) |
|
3 points by kryster 10 months ago | past
|
|
| | Copy and Micropatch: Writing Binary Patches in C with Clang Preserve_none (philipzucker.com) |
|
1 point by gulced 10 months ago | past
|
|
| | Compiling with Constraints (philipzucker.com) |
|
126 points by philzook 10 months ago | past | 36 comments
|
|
| | Copy and Micropatch: Writing Binary Patches in C with Clang Preserve_none (philipzucker.com) |
|
3 points by philzook 10 months ago | past
|
|
| | The C bounded model checker: criminally underused (philipzucker.com) |
|
209 points by philzook 11 months ago | past | 125 comments
|
|
| | Knuckledragger – A Python Experiment on Proof Assistance (philipzucker.com) |
|
1 point by uyasarkocal on Jan 20, 2024 | past
|
|
| | PCode2C: Steps Towards Translation Validation with Ghidra and CBMC (philipzucker.com) |
|
2 points by matt_d on Jan 5, 2024 | past
|
|
| | Knuckledragger: Experimenting with a Python Proof Assistant (philipzucker.com) |
|
3 points by mathgenius on Jan 1, 2024 | past
|
|
| | MiniLitelog: Easy Breezy SQLite Datalog (philipzucker.com) |
|
3 points by philzook on March 12, 2023 | past
|
|
| | Replicating Rise4Fun Z3 with z3-WASM (philipzucker.com) |
|
3 points by hcs on Jan 24, 2023 | past
|
|
| | Datalite: A Simple Datalog Built Around SQLite (philipzucker.com) |
|
4 points by philzook on Oct 7, 2022 | past
|
|
|
|
More |
