[Agda] FRP implementation in Agda

[Alan Jeffrey]

I "borrowed" mainly from Yampa, with a dash of Grapefruit (for the idea 
of tracking signal start times statically using the type system), 
Sculthorpe and Nillson's "Safe FRP through dependent types" (for the 
idea of tracking decoupled functions statically), and Krishnaswami and 
Benton's ultrametric semantics for some of the treatment of fixed points.

A.

On 08/04/2011 03:58 PM, Robin Green wrote:
> Interesting. Which previous FRP approach or approaches would you say
> your library is closest to?
>
> Regards,
> Robin
>
> On Thu, 4 Aug 2011 14:43:46 -0500, Alan Jeffrey<ajeffrey at bell-labs.com>  wrote:
>> Hi everyone,
>>
>> I've recently started work on a Functional Reactive Programming (FRP)
>> library for Agda:
>>
>>     https://github.com/agda/agda-frp-ltl
>>
>> It's early days at the moment, there's lots of gaps and very few
>> combinators, but the basic architecture is in place. The most
>> interesting feature of the library is that it uses a constructive
>> variant of Linear-Time Temporal Logic (LTL) as its type system.
>>
>> The long-term goal is to combine this with the JavaScript back end to
>> allow GUI programs to be written in Agda and executed in the browser.
>>
>> A.