SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Fri 17 Oct 2025 10:45 - 11:00 at Orchid West - Calculus Chair(s): Limin Jia

Graph databases have become an important data management technology across various domains, including biology, sociology, industry, and investigative journalism, due to their ability to efficiently store and query large-scale knowledge graphs and networks. Recently, the Graph Query Language (GQL) was introduced as a new ISO standard providing a unified framework for querying graphs. However, this initial specification lacks a formal type system for query validation. As a result, queries can fail at runtime due to type inconsistencies or produce empty results without prior warning. Solving this issue could have great benefits for users in writing correct queries, especially when handling large datasets.

To address this gap, we introduce a formal type model for a core fragment of GQL extended with property-based filtering and imprecise types both in the schema and the queries. This model, named FPPC, enables static detection of semantically incorrect and stuck queries, improving user feedback. We establish key theoretical properties, including emptiness (detecting empty queries due to type mismatches) and type safety (guaranteeing that well-typed queries do not fail at runtime). Additionally, we prove a gradual guarantee, ensuring that removing type annotations either does not introduce static type errors or only increases the result set. By integrating imprecision into GQL, FPPC offers a flexible solution for handling schema evolution and incomplete type information. This work contributes to making GQL more robust, improving both its usability and its formal foundation.

Fri 17 Oct

Displayed time zone: Perth change

10:30 - 12:15
CalculusOOPSLA at Orchid West
Chair(s): Limin Jia Carnegie Mellon University
10:30
15m
Talk
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
OOPSLA
Chenghang Shi SKLP, Institute of Computing Technology, CAS, Dongjie He Chongqing University, China, Haofeng Li SKLP, Institute of Computing Technology, CAS, Jie Lu SKLP, Institute of Computing Technology, CAS, China, Lian Li Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jingling Xue University of New South Wales
10:45
15m
Talk
Flexible and Expressive Typed Path Patterns for GQL
OOPSLA
Wenjia Ye National University of Singapore, Matías Toro University of Chile, Tomás Diaz University of Chile, Bruno C. d. S. Oliveira University of Hong Kong, Manuel Rigger National University of Singapore, Claudio Gutierrez DCC, Universidad de Chile & IMFD, Domagoj Vrgoč Pontificia Universidad Católica de Chile & IMFD Chile
11:00
15m
Talk
Quantified Underapproximation via Labeled Bunches
OOPSLA
Lang Liu Illinois Institute of Technology, Farzaneh Derakhshan Illinois Institute of Technology, Limin Jia Carnegie Mellon University, Gabriel A. Moreno Carnegie Mellon University Software Engineering Institute, Mark Klein Carnegie Mellon University
11:15
15m
Talk
HpC: A Calculus for Hybrid and Mobile Systems
OOPSLA
Xiong Xu Institute of Software, Chinese Academy of Sciences, Jean-Pierre Talpin INRIA, France, Shuling Wang Institute of Software, Chinese Academy of Sciences, Bohua Zhan Huawei Technologies Co., Ltd., Xinxin Liu Institute of software, Chinese academy of sciences, Naijun Zhan Peking University
11:30
15m
Talk
Notions of Stack-manipulating Computation and Relative Monads
OOPSLA
Yuchen Jiang University of Michigan, Runze Xue University of Michigan; University of Cambridge; Indiana University, Max S. New University of Michigan