Posts tagged with #reactive-programming

← All tags

• FRP in Lean: Composing invariant-transforming combinators

  June 10, 2026

  How do our proofs change as we execute an FRP program?

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

  May 3, 2026

• FRP in Lean: Reactive 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: A Deep Embedding of 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