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

[Wolfgang Jeltsch]

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