Provably Correct Client-Side Web Applications

In this paper, we describe a compiler back end and library for clientside web application development in Agda, a dependently typed functional programming language. The compiler back end targets ECMAScript (also known as JavaScript), and so is executable in a browser. The library is an implementation of Functional Reactive Programming (FRP) using a constructive variant of Linear-time Temporal Logic (LTL) as its type system. The FRP implementation uses the observer pattern for compatibility with the HTML5 event model, using techniques similar to those of self-adjusting computation. The types of FRP signals are used to maintain invariants which allow garbage collection of unused signals, despite the lack of weak pointers or similar capabilities in ECMAScript. We provide Agda bindings for HTML5 DOM nodes and events, and for native ECMAScript arrays and objects. The result is a framework for the development of client-side web applications which supports mechanical verification. Categories and Subject Descriptors D.3.2 [Programming Languages]: Language Classifications--Applicative (functional) languages General Terms Languages Keywords Dependent Types, Functional Reactive Programming, Graphical User Interfaces, Web Programming