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 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
14:00 - 15:30 | Domain-Specific Languages IIPEPM at Room Harbor View Chair(s): Sebastian Erdweg TU Darmstadt, Germany | ||
14:00 30mTalk | BiGUL: A Formally Verified Core Language for Putback-Based Bidirectional Programming PEPM Hsiang-Shang ‘Josh’ Ko National Institute of Informatics, Tao Zan Sokendai, Japan, Zhenjiang Hu National Institute of Informatics DOI Pre-print | ||
14:30 30mTalk | A Constraint Language for Static Semantic Analysis Based on Scope Graphs PEPM Hendrik van Antwerpen Delft University of Technology, Netherlands, Pierre Neron TU Delft, Andrew Tolmach Portland State University, Eelco Visser Delft University of Technology, Guido Wachsmuth Delft University of Technology Link to publication DOI Pre-print | ||
15:00 30mTalk | Finally, Safely-Extensible and Efficient Language-Integrated Query PEPM DOI | ||