Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane

From: Wolfgang Jeltsch <g9ks157k-u9ERN231N2QZkvjqreKGLti2O/JbrIOy <at> public.gmane.org>
Subject: Re: LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs
Newsgroups: gmane.comp.lang.agda
Date: Tuesday 15th November 2011 19:53:48 UTC (over 6 years ago)
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
 
CD: 18ms