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

[Alan Jeffrey]

I'm not surprised that we've discovered this simultaneously, once you 
realize the connection between temporal logic and FRP you wonder why 
this isn't something people learn in elementary school :-)

I'll add a citation to your work to the paper.

A.

On 11/15/2011 01:53 PM, Wolfgang Jeltsch wrote:
> Am Donnerstag, den 10.11.2011, 09:17 -0600 schrieb 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.
>
> Hello,
>
> it’s interesting that you discovered that there is a Curry–Howard
> correspondence between temporal logic and FRP. I’ve also discovered this
> some time ago. You may have a look at the following slides, which are
> from two talks I gave last February:
>
>      The Curry–Howard Correspondence between Temporal Logic and
>      Functional Reactive Programming
>
>          <http://www.cs.ut.ee/~varmo/tday-nelijarve/jeltsch-slides.pdf>
>
>      Programming in Linear Temporal Logic
>
>          <http://cs.ioc.ee/~tarmo/tsem10/jeltsch-slides.pdf>
>
> At the moment, I’m writing a paper about these things.
>
> Best wishes,
> Wolfgang
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda