Philip Zucker
LightNews LightNews
banner
sandmouth.bsky.social
Philip Zucker
@sandmouth.bsky.social
280 followers 340 following 130 posts
Computer Friend, Not a Bird
www.philipzucker.com
Posts Replies Media Videos
Pinned
sandmouth.bsky.social
Philip Zucker @sandmouth.bsky.social · Apr 22
I put a new preprint up summarizing a year or so of fun e-graph ideas. Check it out! #egraphs #logic #compilers arxiv.org/abs/2504.14340
Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching
E-graphs are a data structure for equational reasoning and optimization over ground terms. One of the benefits of e-graph rewriting is that it can declaratively handle useful but difficult to orient i...
arxiv.org
Reposted by Philip Zucker
lawrpaulson.bsky.social
New on my blog:

Set theory with types

lawrencecpaulson.github.io/2025/11/21/T...
Set theory with types
lawrencecpaulson.github.io
November 21, 2025 at 5:01 PM
sandmouth.bsky.social
I've pushed Knuckledragger, my z3 based python proof assistant, up to PyPI pypi.org/project/knuc...
knuckledragger
Interactive Theorem Prover
pypi.org
November 16, 2025 at 3:30 AM
sandmouth.bsky.social
[New Blog Post] Implementing E Unification using SMT www.philipzucker.com/smt_unify/ #logic #automatedreasoning #smt
Implementing E Unification using SMT
Unification is a logical flavored word for the notion of equation solving.
www.philipzucker.com
November 10, 2025 at 8:50 PM
Reposted by Philip Zucker
jalonso.bsky.social
Towards a verified compiler for Distributed PlusCal. ~ Ghilain Bergeron, Horatiu Cirstea, Stephan Merz. hal.science/hal-05329156... #ITP #LeanProver
October 28, 2025 at 12:41 PM
Reposted by Philip Zucker
whitequark.org
please enjoy: my Wasm-hosted, Wasm-targeting build of Clang/Clang++/LLD: a self-contained, 25 MiB (gzipped) pure function
www.npmjs.com/package/@yow...
October 26, 2025 at 9:49 AM
sandmouth.bsky.social
A toy hour clock example proof in a TLA dsl of knuckledragger. Basically combinators over `Int -> T` functions. @hillelwayne.com
October 23, 2025 at 1:52 PM
Reposted by Philip Zucker
jalonso.bsky.social
A gentle introduction to the axiom of choice. ~ Andreas Blass, Dhruv Kulshreshtha. arxiv.org/abs/2509.01830 #Math #SetTheory
A Gentle Introduction to the Axiom of Choice
This article offers a gentle introduction to the axiom of choice. We introduce the axiom, discuss some common objections to it, and present three kinds of reasons to accept it. Although the exposition...
arxiv.org
October 14, 2025 at 9:40 AM
sandmouth.bsky.social
[New Blog Post] ZF style set theory in Knuckledragger I www.philipzucker.com/zf_knuckle1/ #python #logic
ZF style set theory in Knuckledragger I
Zermelo-Fraenkel set theory is a theory of sets.
www.philipzucker.com
October 13, 2025 at 7:38 PM
Reposted by Philip Zucker
jalonso.bsky.social
A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich. arxiv.org/abs/2501.10127 #ITP #IsabelleHOL
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs...
arxiv.org
October 7, 2025 at 3:06 PM
sandmouth.bsky.social
[New Blog Post] Toy Binary Decision Diagrams www.philipzucker.com/toy_bdd/ #python #logic
Toy Binary Decision Diagrams
Binary decision diagrams https://en.wikipedia.org/wiki/Binary_decision_diagram are a data structure for storing boolean functions, spiritually something like [Bool] -> Bool. You can tabulate such a th...
www.philipzucker.com
October 7, 2025 at 1:33 AM
sandmouth.bsky.social
In honor of #racketcon I’ve bolted some quotation onto Knuckledragger github.com/philzook58/k... . Might even be sound!
knuckledragger/src/kdrag/theories/sexp.py at main · philzook58/knuckledragger
A Low Barrier Proof Assistant. Contribute to philzook58/knuckledragger development by creating an account on GitHub.
github.com
October 4, 2025 at 2:14 PM
Reposted by Philip Zucker
hillelwayne.com
Continue to feel like 95% of "why programmers should learn category theory" blogs are really "why programmers should learn abstract algebra"

Which is annoying because there are 1000s of blogs on category theory and 0 on abstract algebra
October 1, 2025 at 2:53 PM
Reposted by Philip Zucker
jalonso.bsky.social
Determinism types for functional logic programming. ~ Michael Hanus, Kai-Oliver Prott. www.michaelhanus.de/publications... #ITP #Rocq
September 29, 2025 at 5:28 PM
Reposted by Philip Zucker
jalonso.bsky.social
Formally verifying a vertical cell decomposition algorithm. ~ Yves Bertot, Thomas Portet. drops.dagstuhl.de/storage/00li... #ITP #Rocq
September 28, 2025 at 2:58 PM
sandmouth.bsky.social
[New Blog Post] Proving the Infinitude of Primes in Knuckledragger #python #logic www.philipzucker.com/knuckle_prim...
Proving the Infinitude of Primes in Knuckledragger
Cody challenged me to prove that there are an infinitely many primes in Knuckledragger, saying it’s the minimum thing to do to demonstrate you have a proof assistant. https://en.wikipedia.org/wiki/Euc...
www.philipzucker.com
September 28, 2025 at 9:05 PM
sandmouth.bsky.social
[New Blog Post] Proof Rules for MetaSMT #python #logic www.philipzucker.com/kdrag_proof_...
Proof Rules for MetaSMT
Knuckledragger https://github.com/philzook58/knuckledragger is my system for interactive theorem proving in python. The core system is not python specific and has some interesting theoretical aspects.
www.philipzucker.com
September 22, 2025 at 9:09 PM
Reposted by Philip Zucker
jalonso.bsky.social
Case study: Verified Vampire proofs in the lambdapi-calculus modulo. ~ Anja Petković Komel, Michael Rawson, Martin Suda. arxiv.org/abs/2503.15541 #ATP #Vampire #ITP #Dedukti
Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
The Vampire automated theorem prover is extended to output machine-checkable proofs in the Dedukti concrete syntax for the LambdaPi-calculus modulo. This significantly reduces the trusted computing ba...
arxiv.org
September 18, 2025 at 10:04 AM
Reposted by Philip Zucker
pqnelson.bsky.social
Read later

arxiv.org/abs/2305.15382
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms...
arxiv.org
September 16, 2025 at 8:42 PM
sandmouth.bsky.social
[New Blog Post] A Slotted Hash Cons for Alpha Invariance www.philipzucker.com/slotted_hash... #hashing #egraph #lambda
A Slotted Hash Cons for Alpha Invariance
Slotted e-graphs https://dl.acm.org/doi/10.1145/3729326 are a data structure that compactly stores many equivalent terms in an alpha invariant aware way. I’ve been very excited by them but also very c...
www.philipzucker.com
September 15, 2025 at 6:07 PM
Reposted by Philip Zucker
jalonso.bsky.social
Stratified datalog and program analysis (in Isabelle/HOL). ~ Anders Schlichtkrull, René Rydhof Hansen, Flemming Nielson. www.isa-afp.org/entries/Stra... #ITP #IsabelleHOL
Stratified Datalog and Program Analysis
Stratified Datalog and Program Analysis in the Archive of Formal Proofs
www.isa-afp.org
September 13, 2025 at 9:43 AM
Reposted by Philip Zucker
michaelgoerz.net
A quick note on Lindblad operators in composite systems. Something I've been confused about for years. #quantum goerz-research.github.io/2025-09-11_C...

Also contains a useful #JuliaLang implementation for a partial trace function, if you ever need that (surprisingly tricky!)
goerz-research.github.io
September 12, 2025 at 4:29 PM
Reposted by Philip Zucker
codyroux.bsky.social
I'm actually kind of proud of this one: open.spotify.com/episode/6LNn...
TREE(3) and the Kruskal theorem
Spotify video
open.spotify.com
September 2, 2025 at 3:14 PM
sandmouth.bsky.social
[New Blog Post] Compositional Datalog on SQL: Relational Algebra of the Environment #datalog #database #sql www.philipzucker.com/compose_data...
Compositional Datalog on SQL: Relational Algebra of the Environment
I spent sone time making Datalogs that translated into SQL. https://www.philipzucker.com/tiny-sqlite-datalog/
www.philipzucker.com
August 26, 2025 at 4:19 AM
sandmouth.bsky.social
[New Blog Post] A Python CLI for Verifying Assembly #formalmethods #assembly #compilers www.philipzucker.com/asm_verify3/
A Python CLI for Verifying Assembly
I’ve been building a system that verifies assembly programs via symbolic execution. I think the following are the most novel points of my approach:
www.philipzucker.com
August 18, 2025 at 3:31 PM
Reposted by Philip Zucker
jalonso.bsky.social
The Vampire diary ~ Filip Bártek et als. arxiv.org/abs/2506.03030 #ATP #Vampire
The Vampire Diary
During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now supports arithmetic,...
arxiv.org
August 15, 2025 at 11:48 AM