BiGUL: A Formally Verified Core Language for Putback-Based Bidirectional Programming
Putback-based bidirectional programming allows the programmer to write only one putback transformation, from which the unique corresponding forward transformation is derived for free. The logic of a putback transformation is more sophisticated than that of a forward transformation and does not always give rise to well-behaved bidirectional programs; this calls for more robust language design to support development of well-behaved putback transformations. In this paper, we design and implement a concise core language BiGUL for putback-based bidirectional programming to serve as a foundation for higher-level putback-based languages. BiGUL is completely formally verified in the dependently typed programming language Agda to guarantee that any putback transformation written in BiGUL is well-behaved.
Tue 19 Jan (GMT-05:00) Guadalajara, Mexico City, Monterrey change
|14:00 - 14:30|
Hsiang-Shang ‘Josh’ KoNational Institute of Informatics, Tao ZanSokendai, Japan, Zhenjiang HuNational Institute of InformaticsDOI Pre-print
|14:30 - 15:00|
Hendrik van AntwerpenDelft University of Technology, Netherlands, Pierre NeronTU Delft, Andrew TolmachPortland State University, Eelco VisserDelft University of Technology, Guido WachsmuthDelft University of TechnologyLink to publication DOI Pre-print
|15:00 - 15:30|