56,966 blogs · [ { "id": "01a08756-bfe4-72b0-b4df-a40c80ff8ae9", "title": "Verifying (simple) C in Isabelle/HOL with AutoCorres", "url": "https://blueberrywren.dev/blog/isabelle-autocorres-tut/", "published_at": "2026-08-28T00:00:00+00:00" }, { "id": "01a08756-bfe4-72b0-b4df-a40c81ae90b0", "title": "Flat/Non-higher-order construction of ANF via mutable holes", "url": "https://blueberrywren.dev/blog/anf-mutable/", "published_at": "2026-05-14T00:00:00+00:00" }, { "id": "01a08756-bfe4-72b0-b4df-a40c829c6d08", "title": "Type safe interpreters", "url": "https://blueberrywren.dev/blog/type-safe-interpreters/", "published_at": "2026-01-17T00:00:00+00:00" }, { "id": "01a08756-bfe4-72b0-b4df-a40c82d9a6d0", "title": "Axiom J in Homotopy Type Theory (HoTT)", "url": "https://blueberrywren.dev/blog/cubical-j/", "published_at": "2026-01-01T00:00:00+00:00" }, { "id": "01a08756-bfe4-72b0-b4df-a40c832164f8", "title": "Written in Pure Sea", "url": "https://blueberrywren.dev/blog/pure-sea/", "published_at": "2025-12-19T00:00:00+00:00" }, { "id": "01a08756-bfe4-72b0-b4df-a40c836e9cc9", "title": "Horrible answers to \"What is a type?\"", "url": "https://blueberrywren.dev/blog/horrible-types/", "published_at": "2025-11-17T00:00:00+00:00" }, { "id": "01a08756-bfe4-72b0-b4df-a40c84340d3e", "title": "Opinion piece: On Zig (and the design choices within)", "url": "https://blueberrywren.dev/blog/on-zig/", "published_at": "2025-10-14T00:00:00+00:00" }, { "id": "01a08756-bfe4-72b0-b4df-a40c8454b35b", "title": "Isabelle/HOL: The various rule methods", "url": "https://blueberrywren.dev/blog/isabelle-rule-musings/", "published_at": "2025-09-19T00:00:00+00:00" }, { "id": "01a08756-bfe5-7094-ab42-23c97fa88483", "title": "Crafting a dependent typechecker, part 1", "url": "https://blueberrywren.dev/blog/dependent-p1/", "published_at": "2025-07-19T00:00:00+00:00" }, { "id": "01a08756-bfe5-7094-ab42-23c97feab096", "title": "Debruijn indexes and levels, and why they're handy", "url": "https://blueberrywren.dev/blog/debruijn-explanation/", "published_at": "2025-05-26T00:00:00+00:00" }, { "id": "01a08756-bfe5-7094-ab42-23c980462bff", "title": "Dependent types suck actually", "url": "https://blueberrywren.dev/blog/dependent-types-suck/", "published_at": "2025-04-01T00:00:00+00:00" }, { "id": "01a08756-bfe5-7094-ab42-23c980613ee4", "title": "A short excerpt on pattern unification", "url": "https://blueberrywren.dev/blog/pattern-unification-short/", "published_at": "2025-03-30T00:00:00+00:00" }, { "id": "01a08756-bfe5-7094-ab42-23c980e997a5", "title": "Welcome back.", "url": "https://blueberrywren.dev/blog/2025-03-27/", "published_at": "2025-03-27T00:00:00+00:00" }, { "id": "01a08756-bfe5-7094-ab42-23c9816354df", "title": "Hi, world.", "url": "https://blueberrywren.dev/blog/first/", "published_at": "2023-06-17T00:00:00+00:00" } ] posts Claim your blog

Blog · corpus.blog/blogs/blueberrywren.dev/posts