## 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## New forum topics |

## Recent comments

16 hours 31 min ago

2 days 17 hours ago

3 days 16 hours ago

4 days 10 hours ago

4 days 19 hours ago

6 days 15 hours ago

6 days 21 hours ago

1 week 8 hours ago

1 week 8 hours ago

1 week 3 days ago