[Agda] Two papers on Agda and FRP

Alan Jeffrey ajeffrey at bell-labs.com
Thu Nov 15 22:04:55 CET 2012


A couple of papers on Agda-related topics that folks here might be 
interested in...

Causality For Free!: Parametricity Implies Causality for Functional 
Reactive Programs. In Proc. ACM Workshop Programming Languages meets 
Program Verification. 2013. 
(http://ect.bell-labs.com/who/ajeffrey/papers/plpv13.pdf)

Dependently Typed Web Client Applications: FRP in Agda in HTML5. In 
Proc. Practical Aspects of Declarative Languages. 2013. 
(http://ect.bell-labs.com/who/ajeffrey/papers/padl13.pdf)

The first paper is part of the formal basis of the agda-frp-js 
implementation of FRP, and uses a parametricity argument to show that 
any implementable function is causal (that is, can't predict the 
future). The second paper is the pragmatic gore behind the 
implementation, and describes the Agda-to-JavaScript compiler, the FFI, 
and the FRP/GUI library.

Both papers are to be presented at satellite workshops of PoPL in January.

Alan.


More information about the Agda mailing list