- A Python Frozenset Interpretation of Dependent Type Theory
by philzook on 5/19/25, 6:18 PM, with comments
- "Verified" "Compilation" of "Python" with Knuckledragger, GCC, and Ghidra
by philzook on 4/8/25, 1:17 PM, with comments
- A Small Prolog on the Z3 AST
by philzook on 4/2/25, 3:50 PM, with comments
- Symbolic Execution by Overloading __bool__
by philzook on 12/24/24, 3:48 AM, with comments
- Higher Order Pattern Unification on the Z3py AST
by philzook on 11/11/24, 10:31 PM, with comments
- Tensors and Graphs: Canonization by Search
by philzook on 11/4/24, 7:42 PM, with comments
- Acyclic Egraphs and Smart Constructors
by philzook on 9/16/24, 11:32 PM, with comments
- String Knuth Bendix
by philzook on 9/9/24, 6:37 PM, with comments
- Ordinals aren't much worse than Quaternions
by philzook on 8/22/24, 3:33 PM, with comments
- Knuckledragger, a Semi-Automated Python Proof Assistant
by philzook on 8/5/24, 2:02 PM, with comments
- Hashing Modulo Theories
by philzook on 5/17/24, 8:51 PM, with comments