corpus.blog
41554 blogs · [ { "id": "01a087b3-a865-70d5-b0b0-326586d6650f", "title": "FRP in Lean: Composing invariant-transforming combinators", "url": "https://dijkstracula.github.io/posts/lean-ltl-6/", "published_at": "2026-06-10T00:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-326586bea188", "title": "FRP in Lean: Stateful combinators, safety, and liveness", "url": "https://dijkstracula.github.io/posts/lean-ltl-5/", "published_at": "2026-05-03T00:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-3265860457ac", "title": "FRP in Lean: Reactive Events and LTL.eventually", "url": "https://dijkstracula.github.io/posts/lean-ltl-4b/", "published_at": "2026-04-24T00:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-32658524f56f", "title": "FRP in Lean: Reactive Signals and LTL.always", "url": "https://dijkstracula.github.io/posts/lean-ltl-4/", "published_at": "2026-04-17T00:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-326584e7f592", "title": "Reactive Programming in Lean Part 3: A Deep Embedding of Linear Temporal Logic", "url": "https://dijkstracula.github.io/posts/lean-ltl-3/", "published_at": "2026-04-02T00:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-326583fbfef4", "title": "Reactive Programming in Lean Part 2: Execution traces", "url": "https://dijkstracula.github.io/posts/lean-ltl-2/", "published_at": "2026-03-15T00:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-3265833f7168", "title": "Reactive Programming in Lean 4", "url": "https://dijkstracula.github.io/posts/lean-ltl/", "published_at": "2026-02-23T00:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-326582ef59cd", "title": "Leaning into the Coding Interview 4: Certified Programming with Proof-Carrying Code", "url": "https://dijkstracula.github.io/posts/proving-the-coding-interview-lean-4/", "published_at": "2026-02-09T05:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-3265827209fe", "title": "Leaning into the Coding Interview: proving equality of different Fuzzbuzzes", "url": "https://dijkstracula.github.io/posts/proving-the-coding-interview-lean-intermezzo/", "published_at": "2026-01-30T05:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-326581d56974", "title": "Leaning into the Coding Interview 3: completing our spec with tacticals and metaprogramming", "url": "https://dijkstracula.github.io/posts/proving-the-coding-interview-lean-3/", "published_at": "2026-01-19T05:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-326581a8ab58", "title": "Leaning Into the Coding Interview 2: static bounds checks and dependent types", "url": "https://dijkstracula.github.io/posts/proving-the-coding-interview-lean-2/", "published_at": "2026-01-11T05:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-326580e9bb0f", "title": "Leaning Into the Coding Interview: Lean 4 vs Dafny cage-match", "url": "https://dijkstracula.github.io/posts/proving-the-coding-interview-lean/", "published_at": "2026-01-02T05:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-326580e7f370", "title": "An Invitation to Liquid Types: Unifying Type Theory and Model Checking", "url": "https://dijkstracula.github.io/posts/liquid-types/", "published_at": "2024-01-15T00:00:00+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-326580246156", "title": "Let's Build a Theorem Prover: Lazy and Basic? SAME", "url": "https://dijkstracula.github.io/posts/lets-build-a-theorem-prover-5/", "published_at": "2023-01-17T20:04:09+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-32658013c9d6", "title": "Let's Build a Theorem Prover: SMT 2: Not(Eq(urne))", "url": "https://dijkstracula.github.io/posts/lets-build-a-theorem-prover-4/", "published_at": "2023-01-05T20:10:48+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-32657fe1169f", "title": "Let's Build A Theorem Prover: Satisfiability Modulo Theory: Digital Deduction Saga", "url": "https://dijkstracula.github.io/posts/lets-build-a-theorem-prover-3/", "published_at": "2022-12-19T16:19:44+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-32657ef6fe3c", "title": "Let's Build a Theorem Prover: SATvatar 2: the way of solver", "url": "https://dijkstracula.github.io/posts/lets-build-a-theorem-prover-2/", "published_at": "2022-12-16T22:02:43+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-32657e82e9a2", "title": "Let's Build a Theorem Prover: Decision procedure lifestyle trends", "url": "https://dijkstracula.github.io/posts/lets-build-a-theorem-prover/", "published_at": "2022-12-07T01:22:23+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-32657e4f61f9", "title": "Proving the Coding Interview: verifying the JDK's `Integer.toString()`", "url": "https://dijkstracula.github.io/posts/proving-the-coding-interview-3/", "published_at": "2022-05-01T01:47:23+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-32657d5c2c3e", "title": "Proving the Coding Interview II", "url": "https://dijkstracula.github.io/posts/proving-the-coding-interview-2/", "published_at": "2022-04-28T14:19:51+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-32657c5c8940", "title": "Proving the Coding Interview", "url": "https://dijkstracula.github.io/posts/proving-the-coding-interview/", "published_at": "2022-04-17T19:18:48+00:00" }, { "id": "01a087b3-a865-70d5-b0b0-32657d2d8705", "title": "Notes on setting up Ivy in Python 3", "url": "https://dijkstracula.github.io/posts/ivy-in-python3/", "published_at": "2022-04-17T19:18:48+00:00" } ] posts Claim your blog
Back to dijkstracula.github.io
Blog · corpus.blog/blogs/dijkstracula.github.io/posts

dijkstracula.github.io

dijkstracula.github.io

2026

FRP in Lean: Composing invariant-transforming combinatorsoriginal ↗
10 Jun 2026
FRP in Lean: Stateful combinators, safety, and livenessoriginal ↗
3 May 2026
FRP in Lean: Reactive Events and LTL.eventuallyoriginal ↗
24 Apr 2026
FRP in Lean: Reactive Signals and LTL.alwaysoriginal ↗
17 Apr 2026
Reactive Programming in Lean Part 3: A Deep Embedding of Linear Temporal Logicoriginal ↗
2 Apr 2026
Reactive Programming in Lean Part 2: Execution tracesoriginal ↗
15 Mar 2026
Reactive Programming in Lean 4original ↗
23 Feb 2026
Leaning into the Coding Interview 4: Certified Programming with Proof-Carrying Codeoriginal ↗
9 Feb 2026
Leaning into the Coding Interview: proving equality of different Fuzzbuzzesoriginal ↗
30 Jan 2026
Leaning into the Coding Interview 3: completing our spec with tacticals and metaprogrammingoriginal ↗
19 Jan 2026
Leaning Into the Coding Interview 2: static bounds checks and dependent typesoriginal ↗
11 Jan 2026
Leaning Into the Coding Interview: Lean 4 vs Dafny cage-matchoriginal ↗
2 Jan 2026

2024

An Invitation to Liquid Types: Unifying Type Theory and Model Checkingoriginal ↗
15 Jan 2024

2023

Let's Build a Theorem Prover: Lazy and Basic? SAMEoriginal ↗
17 Jan 2023
Let's Build a Theorem Prover: SMT 2: Not(Eq(urne))original ↗
5 Jan 2023

2022

Let's Build A Theorem Prover: Satisfiability Modulo Theory: Digital Deduction Sagaoriginal ↗
19 Dec 2022
Let's Build a Theorem Prover: SATvatar 2: the way of solveroriginal ↗
16 Dec 2022
Let's Build a Theorem Prover: Decision procedure lifestyle trendsoriginal ↗
7 Dec 2022
Proving the Coding Interview: verifying the JDK's `Integer.toString()`original ↗
1 May 2022
Proving the Coding Interview IIoriginal ↗
28 Apr 2022
Proving the Coding Intervieworiginal ↗
17 Apr 2022
Notes on setting up Ivy in Python 3original ↗
17 Apr 2022