Posts tagged with #lean

← All tags

• FRP in Lean: Stateful combinators, safety, and liveness

  May 3, 2026

• FRP in Lean: Events and LTL.eventually

  April 24, 2026

  If Signals type to LTL.always, what could type to LTL.eventually?

• FRP in Lean: Reactive Signals and LTL.always

  April 17, 2026

  So if propositions are types, and LTL are propositions, what programs are well-typed by LTL?

• Reactive Programming in Lean Part 3: Linear Temporal Logic

  April 2, 2026

  Specifications that move through time

• Reactive Programming in Lean Part 2: Execution traces

  March 15, 2026

  Recording and reasoning about the states our programs pass through

• Reactive Programming in Lean 4

  February 23, 2026

  Extending Lean's dependent type system to reason about reactive programs

• Leaning into the Coding Interview 4: Certified Programming with Proof-Carrying Code

  February 9, 2026

  Migrating from `List` to `Vector` paid dividends for us being convinced that our Fizzbuzz implementation was correct. Does making our `FB` value type dependent also increase our confidence of correctness?

• Leaning into the Coding Interview: proving equality of different Fuzzbuzzes

  January 30, 2026

  There are lots of different ways to implement Fizzbuzz but this one is mine - how can we prove different implementations are actually the same, and what does it look like when they're actually not?

• Leaning into the Coding Interview 3: completing our spec with tacticals and metaprogramming

  January 19, 2026

  Time to actually write our end-to-end specification!

• Leaning Into the Coding Interview 2: static bounds checks and dependent types

  January 11, 2026

  Pls types? No terms! Only (indexed, dependent) types!

• Leaning Into the Coding Interview: Lean 4 vs Dafny cage-match

  January 2, 2026

  Is Fizzbuzz easier to write in Lean, or just differently hard?