SPLASH 2026
Sat 3 - Fri 9 October 2026 Oakland, California, United States
co-located with SPLASH/ISSTA 2026

The Graph Query Language (GQL), standardized as ISO/IEC 39075 in 2024, is the first international standard for property graph queries. Its semantics, however, is spread across 600+ pages of prose that interleaves data flow, typing, null handling, and syntax/semantics constraints—making the standard difficult to reason about formally or implement correctly. Existing formalizations either retreat to clean algebraic cores—dropping nulls, bags, schemas, and composite queries on multiple graphs—or address only isolated fragments such as path patterns, leaving the full query pipeline unformalized. However, the interplay between expression, pattern and composite query semantics is one of the primary reasons behind GQL’s non-trivial semantics. We present MGQL, the first mechanized, small-step operational semantics for a substantial fragment of GQL. Our formalization models multi-graph property graphs with mixed edge directionality and supports a large spectrum of GQL pattern constructs: quantified paths and edges, directional and undirected matching, label expressions with boolean connectives, and pattern conjunction. MGQL captures the end-to-end query pipeline—graph-site resolution, pattern matching and graph traversal under TRAIL path mode, three-valued null propagation under Kleene logic, aggregation, and composite queries with union, intersection, difference, and otherwise. Complementing the semantics is a schema-aware type system that refines variable types via closed-graph schemas, tracks nullability throughout, supports heterogeneous unions across composite queries, and models quantified-path bindings with list types. We prove layered type soundness: progress and preservation for expressions, schema conformance for patterns, and an end-to-end guarantee that well-typed queries yield binding tables conforming to their declared schemas. Every component is grounded in the ISO/IEC 39075 standard, providing the first rigorous bridge between its prose specification and a mechanized foundation for reasoning about correctness.