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

Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL link.springer.com/article/10.1...

Finally got around to using a treap for my Rust CVM implementation, as Knuth (literally: cs.stanford.edu/~knuth/paper...) intended. Its implementation is compact (~150 LoC, but maybe there's some perf left to wring out of it), but it works real well: crates.io/crates/cvmco...

Starting off uniform circular motion with the whirling stopper is classic but the data can be inconsistent. How might I make the central force more uniform without spending hundreds on dedicated apparatus? #ITeachPhysics

People asked for the rest of the lecture videos for CMU-DB's optimizer course (15799.courses.cs.cmu.edu/spring2025). Unfortunately I got super sick and was in the hospital for 4 weeks. Thankfully @wslim.bsky.social + Jignesh taught the remaining lectures, but we didn't record those classes.

[New Blog Post] Inequality Union Finds: Baby Steps to Refinement E-graphs #compiler www.philipzucker.com/le_find/

A Rocq formalization of simplicial Lagrange finite elements. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. inria.hal.science/hal-05128954... #ITP #Rocq #Math

Next in the Datalog series: writing an optimizer. I used e-graphs to get a feel for how they work, and .. debugging e-graph rules is a lot different from debugging Rust. I really like the idea of forcing myself to use it, and teaching it what rules I think I know. github.com/frankmcsherr...

A gem from Stephen Dolan, which proposes replacing the "generational hypothesis" that drives the design of generational GCs with a notion of lifetime dispersion as measured by the gini coefficient. Nice to see economics playing a role here! dl.acm.org/doi/pdf/10.1...

[New Blog Post] Telescopes Are Tries: A Dependent Type Shellac on SQLite #database #logic www.philipzucker.com/telescope_tr...

[New Blog Post] PLDI 2025 and E-Graphs Modulo Theories Talk www.philipzucker.com/pldi_2025/ @sigplan-pldi.bsky.social

Verified Nanopasses for Compiling Conditionals (draft) www.dropbox.com/scl/fi/cac5j...

Rotating saddle: wait for the end 🤯 #iTeachPhysics

taking a go at oxcaml today first attempt: let's try a parallel reduction. Idea is to compute the "sum" of [f(lo), ..., f(hi-1)] in parallel, combining via some associative function g (and corresponding zero element, z).