[Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs

[Alan Jeffrey]

Hi everyone,

There is now a paper available describing the FRP model I've implemented 
in Agda.

   LTL Types FRP: Linear-time Temporal Logic Propositions as Types,
   Proofs as Functional Reactive Programs. A. S. A. Jeffrey.
   To appear in Proc. ACM Workshop Programming Languages meets
   Program Verification, 2012.
   http://ect.bell-labs.com/who/ajeffrey/papers/plpv12.pdf

The semantics is essentially the same as the JavaScript FRP library, 
although the implementation is quite different.

A.