Thu 11 Jan 2018 15:50 - 16:15 at Bunker Hill - Language Design Chair(s): Zachary Tatlock

Among the frameworks of bidirectional transformations proposed for addressing various synchronisation (consistency maintenance) problems, Foster et al.’s [2007] asymmetric lenses have influenced the design of a generation of bidirectional programming languages. Most of these languages are based on a declarative programming model, and only allow the programmer to describe a consistency specification with ad hoc and/or awkward control over the consistency restoration behaviour. However, synchronisation problems are diverse and require vastly different consistency restoration strategies, and to cope with the diversity, the programmer must have the ability to fully control and reason about the consistency restoration behaviour. The putback-based approach to bidirectional programming aims to provide exactly this ability, and this paper strengthens the putback-based position by proposing the first fully fledged reasoning framework for a bidirectional language — a Hoare-style logic for Ko et al.’s [2016] putback-based language BiGUL. The Hoare-style logic lets the BiGUL programmer precisely characterise the bidirectional behaviour of their programs by reasoning solely in the putback direction, thereby offering a unidirectional programming abstraction that is reasonably straightforward to work with and yet provides full control not achieved by previous approaches. The theory has been formalised and checked in Agda, but this paper presents the Hoare-style logic in a semi-formal way to make it easily understood and usable by the working BiGUL programmer.

Slides (POPL18.pdf)695KiB

Thu 11 Jan

15:50 - 16:40: Research Papers - Language Design at Bunker Hill
Chair(s): Zachary TatlockUniversity of Washington
POPL-2018-papers15:50 - 16:15
Hsiang-Shang ‘Josh’ KoNational Institute of Informatics, Japan, Zhenjiang HuNational Institute of Informatics
Link to publication DOI Pre-print Media Attached File Attached
POPL-2018-papers16:15 - 16:40
Martin OderskyEPFL, Switzerland, Olivier BlanvillainEPFL, Fengyun LiuEPFL, Switzerland, Aggelos BiboudisEcole Polytechnique Federale de Lausanne, Heather MillerEcole Polytechnique Federale de Lausanne, Sandro StuckiEPFL