41554 blogs · [ { "id": "01a0da74-135d-72fe-8a2b-dac71c5a42cf", "title": "A Lean Proof Printing Python Union Find", "url": "https://www.philipzucker.com/proof_uf/", "published_at": "2026-09-25T00:00:00+00:00" }, { "id": "01a0cdc6-9645-7006-be5a-cb3bef2240b6", "title": "Lambda MicroEgg", "url": "https://www.philipzucker.com/lambda_miller_egg/", "published_at": "2026-09-20T00:00:00+00:00" }, { "id": "01a0bdce-5b3f-71a3-9f26-c20699861f57", "title": "Lean Metaprogramming Etudes: Execution is Elaboration", "url": "https://www.philipzucker.com/elab_lean/", "published_at": "2026-09-13T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e14fcab084d", "title": "Validating GDB Interrupt Traces Against a TLA+ Spec", "url": "https://www.philipzucker.com/tla_traces/", "published_at": "2026-09-04T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e14fd2f521b", "title": "Grobner / Buchberger / Knuth Bendix for Semirings and Seven Trees in One", "url": "https://www.philipzucker.com/type_algebra_semiring/", "published_at": "2026-08-21T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e14fd748a07", "title": "An Intuitionistic Micro Proof Assistant", "url": "https://www.philipzucker.com/kd_intu/", "published_at": "2026-08-07T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e14fe3ca538", "title": "Finite Algebraic Effects as dicts and such", "url": "https://www.philipzucker.com/bdd_term_alg_effects/", "published_at": "2026-07-29T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e14feb4eea4", "title": "Making TLA+ and x86 Kiss Via Z3Py", "url": "https://www.philipzucker.com/kissin_tla/", "published_at": "2026-07-17T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e14ff189ff0", "title": "Lifting Terms: Making Well Scoped Syntax Dumber", "url": "https://www.philipzucker.com/thin_term/", "published_at": "2026-07-10T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e14ffa49b21", "title": "A Theory of Arrays (ToA) Union Find", "url": "https://www.philipzucker.com/toa_unionfind/", "published_at": "2026-07-03T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e14ffeacb30", "title": "Arenas, Cyclic Terms, and Flat Equational Systems", "url": "https://www.philipzucker.com/arena_coegraph2_rational/", "published_at": "2026-06-01T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e1500ab1eae", "title": "Lifting E-Graphs", "url": "https://www.philipzucker.com/lifting_egraph/", "published_at": "2026-05-25T00:00:00+00:00" }, { "id": "01a087c2-0ac1-71a5-ba67-2e150119f89b", "title": "Reading Proof Objects and Completed Rewrite Systems from eprover into Knuckledragger", "url": "https://www.philipzucker.com/proof_processing/", "published_at": "2026-05-17T00:00:00+00:00" } ] posts Claim your blog

Back to Hey There Buddo! | Hot Leaves in a Cold Worlds.

Blog · corpus.blog/blogs/philipzucker.com/posts

Hey There Buddo! | Hot Leaves in a Cold Worlds.

philipzucker.com

2026

A Lean Proof Printing Python Union Find original ↗

25 Sept 2026

Lambda MicroEgg original ↗

20 Sept 2026

Lean Metaprogramming Etudes: Execution is Elaboration original ↗

13 Sept 2026

Validating GDB Interrupt Traces Against a TLA+ Spec original ↗

4 Sept 2026

Grobner / Buchberger / Knuth Bendix for Semirings and Seven Trees in One original ↗

21 Aug 2026

An Intuitionistic Micro Proof Assistant original ↗

7 Aug 2026

Finite Algebraic Effects as dicts and such original ↗

29 Jul 2026

Making TLA+ and x86 Kiss Via Z3Py original ↗

17 Jul 2026

Lifting Terms: Making Well Scoped Syntax Dumber original ↗

10 Jul 2026

A Theory of Arrays (ToA) Union Find original ↗

3 Jul 2026

Arenas, Cyclic Terms, and Flat Equational Systems original ↗

1 Jun 2026

Lifting E-Graphs original ↗

25 May 2026

Reading Proof Objects and Completed Rewrite Systems from eprover into Knuckledragger original ↗

17 May 2026