Abstract

Functional reactive programming (FRP) languages are concise and expressive, but also can be tricky for users to write and debug; the wide space of possible inputs often results in unforeseen corner cases. We propose synthesizing FRP programs using partial specifications and an interactive refinement loop in which the user disambiguates candidate programs until one that is correct on all inputs is found. To make synthesis tractable, we present a reduction of asynchronous inputs (referred to in FRP as event streams and behaviors) to lists of values. We show that our model gives good performance by authoring benchmark programs using CEGIS-style synthesis over a grammar that contains a variety of operators, including first-class functions.

Video Recording