Posts tagged with #frp
-
FRP in Lean: Composing invariant-transforming combinators
How do our proofs change as we execute an FRP program?
-
FRP in Lean: Stateful combinators, safety, and liveness
-
FRP in Lean: Reactive Events and LTL.eventually
If Signals type to LTL.always, what could type to LTL.eventually?
-
FRP in Lean: Reactive Signals and LTL.always
So if propositions are types, and LTL are propositions, what programs are well-typed by LTL?