Workshop on Bidirectional Computation and Its Application

Theories and Frameworks for Trustworthy Development of Ubiquitous Information Systems Based on Bidirectional Computing

00 Days
00 Hours
00 Minutes
00 Seconds

Introduction

Welcome to the Workshop on Bidirectional Computation and Its Application! This workshop aims to bring together leading scholars to engage in in-depth presentations and discussions centered on the project's core objective—leveraging the advanced concept of "bidirectional computing" to construct a comprehensive trusted development framework spanning from formal theories to engineering practices. The workshop is designed to establish a high-level, international academic dialogue platform for discussing cutting-edge issues, sharing interim research findings, and planning future collaborative research directions.
This workshop is partially supported by the National Natural Science Foundation of China (NSFC) under its project "Theories and Frameworks for Trustworthy Development of Ubiquitous Information Systems Based on Bidirectional Computing".

Date

December 06 - December 09, 2025

Location

Meeting Room 1, Building 1
Zhongguan Xinyuan
Haidian District, Beijing
Open Location in Google Maps

Program

December 07

9:00 - 9:30: Hu, Zhenjiang, Opening Remarks

Session 1 (Chair: Hu, Zhenjiang)

9:30 - 10:10: Makoto Onizuka, Read-Visible Serializability and Scalable Transaction Processing
10:10 - 10:50: Xie, Ruifeng, Effectful Lenses: There and Back with Different Monads
10:50 - 11:30: Soichiro Hidaka, Change Managements among Multiple Information Sources using Bidirectional Transformations and Operational Transformations

Session 2 (Chair: Makoto Onizuka)

14:00 - 14:40: Yasunori Ishihara, Static Analysis of BX-based Data Sharing
14:40 - 15:20: Guo, Guanchen, Derivative-based Bidirectional Programming

15:20 - 15:40: Coffee Break

Session 3 (Chair: Soichiro Hidaka)

15:40 - 16:20: Zan, Tao, LiveCSS: Direct Manipulation of Computed Styles
16:20 - 17:00: Wang, Fusen, AsyncLens: Towards Eventual Consistency between Source and View under Concurrent Updates

December 08

Session 4 (Chair: Xiong, Yingfei)

9:00 - 9:40: Hiroyuki Kato, Towards Translating SQL View Update Statements
9:40 - 10:20: Guan, Zhichao, Language Lifting for Domain-Specific Language Development
10:20 - 11:00: He, Xiao, Model-Text Synchronization in SysML v2: Requirements, Solutions, and Reflections

13:00 - 15:00: Project Discussion(Host: Hu, Zhenjiang)

Talk Details (Alphabetical Order)

He, Xiao (University of Science and Technology Beijing), Model-Text Synchronization in SysML v2: Requirements, Solutions, and Reflections
Abstract: SysML v2 is the latest standard modeling language for model-based system engineering (MBSE). One of its core features is that SysML v2 provides both graphical and textual syntax. This feature poses a key challenge in tool implementation: synchronizing graphical and textual representations. In this presentation, I will outline the major requirements for this synchronization problem, encountered by my industrial collaborators and me during next-generation SysML tool development, and propose our solution blueprint for achieving this synchronization. Particularly, I will focus on my latest work on BIT (Bidirectional Incremental Transformation), a template-based approach for incremental and bidirectional model-to-text transformation, which serves as the key component in our solution. Finally, I will identify the remaining challenges and share reflections on applying bidirectional (model-to-text) transformation in industrial settings for discussions.
Hiroyuki Kato (NII), Towards Translating SQL View Update Statements
Abstract: The view update problem is a long-standing challenge in database research: how can updates applied to database views be correctly translated into corresponding updates on the underlying base relations? This problem is complicated by the fact that multiple possible base updates may correspond to a single view modification. Recent work has approached this challenge using bidirectional transformation (BX) techniques, a framework that has been extensively studied in the programming languages community. BX offers a rigorous foundation by ensuring well-behavedness (i.e., side-effect-freeness) of updates. However, applying BX principles directly to practical database systems remains a nontrivial task. A key difficulty lies in a fundamental assumption of BX—that updates are performed on free-standing views, which are independent, in-memory structures rather than persistent database objects. In contrast, real-world database applications interact with views just as they do with base tables, typically without distinguishing between them. Since data modifications in relational systems are carried out via standard SQL statements (e.g., INSERT, DELETE, UPDATE), achieving updatable views through these same mechanisms is essential for practical deployment. In this talk, I will present our ongoing work towards translating SQL view update statements in a way that preserves well-behavedness, aiming to bridge the gap between theoretical BX frameworks and practical database implementations.
Guan, Zhichao (Peking University), Language Lifting for Domain-Specific Language Development
Abstract: As software development continues to evolve, domain-specific languages (DSLs) have become essential tools for addressing targeted problems. Although embedded DSLs can reduce development costs, characteristics of the host language often leak into use, undermining the DSL’s purity and simplicity. This report presents a Language Lifting technique that takes the host-language specification and DSL-to-host translation as inputs to automatically infer the DSL’s specification and rigorously enforce its abstraction boundaries.
Guo, Guanchen (Peking University), Derivative-based Bidirectional Programming
Abstract: Approaches to developing BXs can be mainly categorized into get-based and put-based approaches, enabling us to define a get or put function from which a complete BX can be automatically constructed. Nevertheless, the get-based approaches suffer from the ambiguity issues, while put-based approaches face complexity issues due to the requirement of managing source-view alignment explicitly. In this talk, we introduce derivative-based bidirectional programming, where BX is specified through get′, the derivative of get. This approach enables BXs to be constructed directly by integration and right inverse. It is more intuitive to write than traditional put-based approaches, since developers specify only the forward transformation from source to view without manually designing view–source alignments. At the same time, it offers better control over the backward transformation than purely get-based approaches. We further design dBX, a domain-specific language for expressing derivatives. It eliminates the need for explicit view–source alignment while allowing developers to design different backward transformations for the same forward specification. Finally, we implement a prototype tool to execute dBX programs, and demonstrate that our approach is both expressive and practical.
Makoto Onizuka (The University of Osaka), Read-Visible Serializability and Scalable Transaction Processing
Abstract: We propose Read-Visible Serializability (RVSR), a generalized transactional semantics unifying CRDT/OT reconciliation with database-level guarantees for user-visible reads. Unlike CSR or VSR, RVSR only requires each visible read to reflect a serial prefix of a total order over effects under a deterministic reconciliation policy ρ. We formalize RVSR, place it in the hierarchy CSR ⊂ VSR ⊂ RVSR ⊂ FSR, and prove an equivalent ρ-based characterization. Using return-value commutativity (RVC), we derive a sufficient condition for merged-state equivalence and provide an SMT-based RVC checker. We implement these semantics in Auto-CRDT Planner, which compiles SQL to an effects IR and automatically selects (i) CRDT rewriting, (ii) key-local coordination for ordered updates, or (iii) serializable fallback. On TPC-C workloads, Auto achieves much higher throughput than 2PL while preserving correctness through PN-counters, escrow-based decrements, and merge-then-read snapshots. RVSR thus offers a principled foundation for safe, scalable reconciliation across transactional and CRDT systems.
Soichiro Hidaka (Hosei University), Change Managements among Multiple Information Sources using Bidirectional Transformations and Operational Transformations
Abstract: Multidirectional transformations maintain consistency among more than two information sources. They are expected to play an important role in collaborative data sharing. Bidirectional transformations have been applied for such scenario by architectures such as Dejima and BCDS. Assuming Dejima architecture as bipartite network of bidirectional transformations in which base tables and views constitute two sets of nodes while bidirectional transformations correspond to the edges between base tables and views, we have developed an evolutionary framework to cope with various reconfigurations such as joining of new nodes and reconciliation among bidirectional transformations having different ranges while incoming common nodes. Although such framework seems promising, we still have challenges such as reconciliation of conflicting updates in such nodes. We could approach this problem by operational transformations to merge such updates. However, since the resultant state after the merging is different in general from the result of applying any one of these update only. That causes weakening of synchronization property even if each component bidirectional transformation satisfy strong round-tripping property called PutGet. In this presentation, we recap the evolutionary framework and briefly discuss the challenges related to the conflict resolution problem. We also would like to introduce some of the efforts related to change managements in the Infrastructure Software Laboratory led by the presenter in Hosei University.
Wang, Fusen (Peking University), AsyncLens: Towards Eventual Consistency between Source and View under Concurrent Updates
Abstract: Lenses are used to maintain consistency between a high-information source and a low-information view, offering benefits like compositional programming and information hiding. However, existing lenses are unsuitable for modern collaborative applications. When a source and a view are modified concurrently, existing approaches cannot merge both changes and typically discard one which is a critical failure for collaboration. This talk introduces lenses over CRDTs, a novel framework designed to solve this problem. Its primary goal is to ensure that the source-view pair merges concurrent modifications from both sides and achieves Eventual Consistency (EC). We present a theoretical framework that formally defines correctness and EC properties for this new class of lenses. Within this framework, we identify monotonicity as a key sufficient condition that, when combined with correctness, guarantees EC. We then instantiate this theory by designing a rich combinator language for tree-structured CRDTs, proving that our combinators preserve these properties by construction. Finally, we demonstrate the practical application of our framework by implementing CAT, a collaborative tree-structured data editor that supports collaboration on distinct but associated data, and and validating our design with a non-trivial case study.
Xie, Ruifeng (Peking University), Effectful Lenses: There and Back with Different Monads
Abstract: Bidirectional transformations (BXs) are a widely adopted approach for data synchronisation that is usually based on two functions, one from the source to the view and one back. Traditionally, these functions must not have side effects. While a few frameworks aim to lift this restriction by introducing monads into lenses, they are still quite limited, e.g., allowing only side effects in the backwards transformation. In this paper, we propose a much more general framework for effectful lenses. Our effectful lenses can have different effects in their two directions, and the effects need not be cancellable. We also define the round-trip relations and use them to generalise the two well-known round-trip properties to effectful lenses. Moreover, composition preserves the two well-known round-trip properties, and we also provide a rich combinator language, which enables compositional programming for effectful lenses. Finally, we present a case study to illustrate the flexibility and expressivity of our framework.
Yasunori Ishihara (Nanzan University), Static Analysis of BX-based Data Sharing
Abstract: This presentation discusses two topics related to the static analysis of BX-based data sharing. The first topic is consistency checking of a given BX (more specifically, a given putback function) for relational data against given functional dependencies. Assuming that the get function corresponds to a SPJ (select-project-join) query, we focus on two types of putback functions, namely, "less-source-change put" and "least-source-size put." Then, we show decidable necessary and sufficient conditions for a given putback function to never violate given functional dependencies of the source schema. The second topic is confidentiality checking of the Dejima architecture, which was proposed by the BISCUITS project. We first define confidentiality on the Dejima architecture, and then discuss the conditions under which this confidentiality property is decidable.
Zan, Tao (Longyan University), LiveCSS: Direct Manipulation of Computed Styles
Abstract: In conventional web development, the workflow of CSS editing is unidirectional: developers modify the source code, reload the page, and repeatedly inspect the rendered result until the visual outcome meets expectations. This trial-and-error process is inefficient, as any visual adjustment requires returning to the source and re-executing the entire rendering pipeline. We introduce LiveCSS, a bidirectional stylesheet execution framework that enables direct modification of visual results. Instead of editing the source first, developers can interactively adjust the rendered appearance—such as layout, color, or spacing—and have the system automatically infer and propagate corresponding changes back to the original CSS source. LiveCSS formalizes this process as a pair of forward and backward semantics, where the forward direction computes visual styles and the backward direction reconstructs source updates from output edits.

Meals

Midday Meal

Zhongguan Xinyuan
Haidian District, Beijing

Evening Meal

Huajia Yiyuan
Haidian District, Beijing

Attendees

Committee (Alphabetical Order)

Contact

For inquiries, please contact us at:

yecui at pku.edu.cn
wangjianjia at pku.edu.cn