[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