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

Displayed time zone: Tijuana, Baja California change

15:50 - 16:40
Language DesignResearch Papers at Bunker Hill
Chair(s): Zachary Tatlock University of Washington, Seattle
An Axiomatic Basis for Bidirectional Programming
Research Papers
Hsiang-Shang ‘Josh’ Ko National Institute of Informatics, Japan, Zhenjiang Hu National Institute of Informatics
Link to publication DOI Pre-print Media Attached File Attached
Simplicitly: Foundations and Applications of Implicit Function Types
Research Papers
Martin Odersky EPFL, Switzerland, Olivier Blanvillain EPFL, Fengyun Liu EPFL, Switzerland, Aggelos Biboudis Ecole Polytechnique Federale de Lausanne, Heather Miller Ecole Polytechnique Federale de Lausanne, Sandro Stucki EPFL