Just out: Functional Data Structures, edited by Tobias Nipkow

New on my blog: Set theory with types lawrencecpaulson.github.io/2025/11/21/T...

I've pushed Knuckledragger, my z3 based python proof assistant, up to PyPI pypi.org/project/knuc...

[New Blog Post] Implementing E Unification using SMT www.philipzucker.com/smt_unify/ #logic #automatedreasoning #smt

Towards a verified compiler for Distributed PlusCal. ~ Ghilain Bergeron, Horatiu Cirstea, Stephan Merz. hal.science/hal-05329156... #ITP #LeanProver

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...

A toy hour clock example proof in a TLA dsl of knuckledragger. Basically combinators over `Int -> T` functions. @hillelwayne.com

A gentle introduction to the axiom of choice. ~ Andreas Blass, Dhruv Kulshreshtha. arxiv.org/abs/2509.01830 #Math #SetTheory

[New Blog Post] ZF style set theory in Knuckledragger I www.philipzucker.com/zf_knuckle1/ #python #logic

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

[New Blog Post] Toy Binary Decision Diagrams www.philipzucker.com/toy_bdd/ #python #logic

In honor of #racketcon I’ve bolted some quotation onto Knuckledragger github.com/philzook58/k... . Might even be sound!

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

Determinism types for functional logic programming. ~ Michael Hanus, Kai-Oliver Prott. www.michaelhanus.de/publications... #ITP #Rocq

Formally verifying a vertical cell decomposition algorithm. ~ Yves Bertot, Thomas Portet. drops.dagstuhl.de/storage/00li... #ITP #Rocq

[New Blog Post] Proving the Infinitude of Primes in Knuckledragger #python #logic www.philipzucker.com/knuckle_prim...

[New Blog Post] Proof Rules for MetaSMT #python #logic www.philipzucker.com/kdrag_proof_...

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

Read later arxiv.org/abs/2305.15382

[New Blog Post] A Slotted Hash Cons for Alpha Invariance www.philipzucker.com/slotted_hash... #hashing #egraph #lambda

Stratified datalog and program analysis (in Isabelle/HOL). ~ Anders Schlichtkrull, René Rydhof Hansen, Flemming Nielson. www.isa-afp.org/entries/Stra... #ITP #IsabelleHOL

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!)

I'm actually kind of proud of this one: open.spotify.com/episode/6LNn...

[New Blog Post] Compositional Datalog on SQL: Relational Algebra of the Environment #datalog #database #sql www.philipzucker.com/compose_data...

[New Blog Post] A Python CLI for Verifying Assembly #formalmethods #assembly #compilers www.philipzucker.com/asm_verify3/

The Vampire diary ~ Filip Bártek et als. arxiv.org/abs/2506.03030 #ATP #Vampire

Second analysis lecture "Filter" (June 17, 2025). ~ Alex Kontorovich. alexkontorovich.github.io/2025SimonsFo... #ITP #LeanProver #Math

[New Blog Post] Knuckledragger Analysis Etudes www.philipzucker.com/knuckle_anal...

[New Blog Post] Semantic Refinement/Dependent Typing for Knuckledragger/SMTLIB Pt 1 www.philipzucker.com/refinement_k... #types #smt

Isle 🏝️ is my new #FPGA project. Isle is a simple, modern computer — an open design that encourages tinkering, experimentation, and doing your own thing. I hope to inspire you to come on a journey with me and build your own computer. projectf.io/isle/fpga-co...

[New Blog Post] Verified Assembly 2: Memory, RISC-V, Cuts for Invariants, and Ghost Code www.philipzucker.com/asm_verify2/ #ghidra #assembly

Another homotopy blog post. bartoszmilewski.com/2025/07/26/w...

... Well. I got a paper number, despite thinking I'd just hold onto it. No wording but I think it's about as complete as it can be. thephd.dev/_vendor/futu...

Something I think is interesting about Knuckledragger is that the meta (python) is very different than the object language (HOL/SMTLIB).

[New Blog Post] Semi-Automated Assembly Verification in Python using pypcode Semantics #ghidra #assembly www.philipzucker.com/assembly_ver...

The calculated typer (Functional Pearl). ~ Zac Garby, Patrick Bahr, Graham Hutton. people.cs.nott.ac.uk/pszgmh/typer... #Haskell #FunctionalProgramming

Teaching software specification (Experience report). ~ Cameron Moy, Daniel Patterson. ccs.neu.edu/~camoy/pub/l... #CompSci #Teaching #ITP #LeanProver #ACL2

Tom Smeding, Miko{\l}aj Konarski, Simon Peyton Jones, Andrew Fitzgibbon Dual-Numbers Reverse AD for Functional Array Languages https://arxiv.org/abs/2507.12640

A simple formalization of alpha-equivalence. ~ Kalmer Apinis, Danel Ahman. arxiv.org/abs/2507.10181 #ITP #Rocq

Great blogpost about partial evaluation / futamura projections applied to WASM: cfallin.org/blog/2024/08...

I first wrote up the idea for this 6 years ago, but it took a huge amount of work to actually turn it into reality. Thank you to Orion for the heavy lifting, and all the other Automerge contributors for making it happen!

Exploiting instantiations from paramodulation proofs in Isabelle/HOL. ~ Lukas Bartl, Jasmin Blanchette, Tobias Nipkow. www.tcs.ifi.lmu.de/mitarbeiter/... #ITP #IsabelleHOL

i love c++ mcyoung.xyz/2025/07/14/b...

[New Blog Post] Using Lean like an External SMT Solver from Python www.philipzucker.com/lean_smt/ #LeanLang @lean-lang.org

New blog post on implementing patchelf-like functionalities using LIEF's Rust bindings: lief.re/blog/2025-07...

Read later arxiv.org/abs/2507.06360

May 25-27, 2025, I hosted an event, the "Minnowbrook Logic Programming Seminar," in Blue Mountain Lake, NY. I recorded 11 talks on Datalog-related interests, totaling over 9+ hours of video, which I have just now published on YouTube youtu.be/3ec9VfMUVa8

[New Blog Post] Doing Lean Dirty: Lean as a Jupyter Notebook Replacement www.philipzucker.com/dirty_lean/ #lean4

Markus Himmel has written a blog post about how to write a simple imperative program in Lean and then how to verify that the program is bug-free. markushimmel.de/blog/my-firs...