An Axiomatic Basis for Bidirectional Programming

Watch a 24-minute conference presentation from POPL 2018 exploring the development of a Hoare-style logic framework for the putback-based bidirectional programming language BiGUL. Learn how this novel approach enables programmers to precisely control and reason about consistency restoration behavior in bidirectional transformations, moving beyond the limitations of previous declarative programming models. Discover how the framework allows developers to characterize bidirectional behavior by reasoning solely in the putback direction, providing a straightforward yet powerful unidirectional programming abstraction. The talk covers the theoretical foundations, which have been formally verified in Agda, while presenting the logic in an accessible way for practical application by BiGUL programmers working on synchronization and consistency maintenance challenges.