Posts tagged with #reactive-programming

← 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