A Formally Verified Core Language for Putback-based Bidirectional Programming

Putback-based bidirectional programming allows us to write only one putback transformation, from which the unique corresponding forward transformation is derived for free. Although a putback transformation has full control of bidirectional behaviour, its logic is more sophisticated than that of a forward transformation and does not always give rise to well-behaved bidirectional programs. This calls for design of robust programming languages to support development of well-behaved putback transformations. In this paper, we design and implement a concise language for putback-based bidirectional programming, which is not only expressive enough to serve as the core for higher-level putback-based languages, but also completely formally verified to guarantee that any putback transformation written in the language is well-behaved.
Team Members

Thanks to all members in our PRL lab for intensive discussion and useful comments.