An Intuitionistic Micro Proof Assistant
I’ve been tinkering on a solver-oriented interactive proof assistant as a library called Knuckledragger https://github.com/philzook58/knuckledragger .
Hey There Buddo!
A blog about life, programming, math, logic, and physics.
Latest posts
Finite Algebraic Effects as dicts and such
Algebraic effects are a style / mathematical framework for modelling mutation, search, and some other things. They are another attempt to bridge the gap between mathy looking stuff and our crass world of mud and time.
Making TLA+ and x86 Kiss Via Z3Py
I’ve been trying my hand at translating a reasonable subset of TLA+ into z3py for the purposes of connecting specs to Verus, CBMC, and my assembly checker and also for maybe a little interactive theorem proving as a treat.
Lifting Terms: Making Well Scoped Syntax Dumber
I have been writing posts about Lifting Egraphs video as an intriguing way of adding variables and scope into an egraph. But pulling back a little, I can see that the simpler thing to talk about first is lifting terms.
A Theory of Arrays (ToA) Union Find
One thing I’ve been discussing with Rudi, Michel and Max is union find annotations. Union find enhancements that still feel like union finds.
Arenas, Cyclic Terms, and Flat Equational Systems
I was invited a few months ago into discussions with Cheng Zhang, Sam Coward and Alexandra Silva on some work integrating loopy infinite streamy things into e-graphs. A few years back, I was barking up a similar but distinct tree https://www.philipzucker.com/coegraph/
Lifting E-Graphs
I submitted a talk to the EGRAPHS workshop and it was accepted! https://pldi26.sigplan.org/details/egraphs-2026-papers/13/Lifting-E-Graphs-A-Function-Isn-t-a-Constant
Reading Proof Objects and Completed Rewrite Systems from eprover into Knuckledragger
Automated reasoning is fun.
Family Orienting Python Frozenset Dependent Type Theory
I like trying to finitize things and put them in mundane trappings.
Lifting and Lowering Functions with The Dump Calculus
I’ve been trying to think about how to make a nameless de bruijn-y e-graph and that has led me down a road to consider some interesting functional combinators for lifting and lowering functions.