## User login## Navigation |
## LTL types FRP
Alan Jeffrey (to appear 2012) LTL types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs. To be presented at next year's
Programming Languages meets Program Verification, (PLPV 2012).
Functional Reactive Programming (FRP) is a form of reactive programming whose model is pure functions over signals. FRP is often expressed in terms of arrows with loops, which is the type class for a Freyd category (that is a premonoidal category with a cartesian centre) equipped with a premonoidal trace. This type system sufï¬ces to deï¬ne the dataï¬‚ow structure of a reactive program, but does not express its temporal properties. In this paper, we show that Linear-time Temporal Logic (LTL) is a natural extension of the type system for FRP, which constrains the temporal behaviour of reactive programs. We show that a constructive LTL can be deï¬ned in a dependently typed functional language, and that reactive programs form proofs of constructive LTL properties. In particular, implication in LTL gives rise to stateless functions on streams, and the â€œconstrainsâ€ modality gives rise to causal functions. We show that reactive programs form a partially traced monoidal category, and hence can be given as a form of arrows with loops, where the type system enforces that only decoupled functions can be looped.Via Alan's G+ feed. |
## Browse archives## Active forum topics |

## Recent comments

7 hours 24 min ago

9 hours 28 min ago

10 hours 46 min ago

11 hours 32 min ago

11 hours 55 min ago

12 hours 5 min ago

13 hours 4 min ago

13 hours 25 min ago

14 hours 36 min ago

23 hours 10 min ago