[Agda] Functional Reactive Types

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Congrats to your accepted paper!

On 31.03.2014 22:32, Alan Jeffrey wrote:
> Hi everyone,
> 
> A paper about FRP formalized in Agda:
> 
> Functional Reactive Types A. S. A. Jeffrey. To appear in Proc.
> EACSL Computer Science Logic / IEEE Logic in Computer Science.
> 2014. http://ect.bell-labs.com/who/ajeffrey/papers/lics14.pdf
> 
> The summary is that FRP streams of values [v1,v2,...] can
> naturally typed using a stream of types [A1,A2,...] where each vi
> has type Ai. This means that functions on streams of types can be
> used to give the types of functions on streams of values. For
> example the tail function takes a stream [v1,v2,...] of type
> [A1,A2,...] and gives back the stream [v2,v3,...] of type
> [A2,A3,...] so its type can be considered to be (tail : [As] ->
> [tail(As)]). The paper discusses a minimal FRP library (head, tail,
> cons, induction, and applicative functor) and shows that it is
> enough to type itself, and to define a constructive past-time LTL.
> 
> Of particular interest to this mailing list may be the Agda
> sources themselves
> (http://ect.bell-labs.com/who/ajeffrey/papers/lics14.tgz) since
> they use a collection of LaTeX and Agda trickery to allow the paper
> to be a Literate Agda development where the Agda (hopefully) 
> doesn't get in the way too much.
> 
> Alan. _______________________________________________ Agda mailing
> list Agda at lists.chalmers.se 
> https://lists.chalmers.se/mailman/listinfo/agda
> 


- -- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iEYEARECAAYFAlM60j0ACgkQPMHaDxpUpLO93QCfUTW1hg7Z2PbZwancQDfGvKX8
IlYAn3Z/q9enwvOllDqT+N+FuXKN7f03
=1xmb
-----END PGP SIGNATURE-----