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 7 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 |
|||