I get a 404 on that link.<br><br><div class="gmail_quote">On 10 November 2011 15:17, Alan Jeffrey <span dir="ltr">&lt;<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi everyone,<br>
<br>
There is now a paper available describing the FRP model I&#39;ve implemented in Agda.<br>
<br>
  LTL Types FRP: Linear-time Temporal Logic Propositions as Types,<br>
  Proofs as Functional Reactive Programs. A. S. A. Jeffrey.<br>
  To appear in Proc. ACM Workshop Programming Languages meets<br>
  Program Verification, 2012.<br>
  <a href="http://ect.bell-labs.com/who/ajeffrey/papers/plpv12.pdf" target="_blank">http://ect.bell-labs.com/who/<u></u>ajeffrey/papers/plpv12.pdf</a><br>
<br>
The semantics is essentially the same as the JavaScript FRP library, although the implementation is quite different.<br>
<br>
A.<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div><br>