Posts tagged with #ltl
-
FRP in Lean: Stateful combinators, safety, and liveness
-
FRP in Lean: 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?
-
Reactive Programming in Lean Part 3: Linear Temporal Logic
Specifications that move through time