一句话：提出 MGQL：GQL 只读子片段的首个机械化小步操作语义与可靠类型系统，连接 ISO 39075 标准与可执行实现。
ISO/IEC 39075（2024）标准化了属性图查询语言 GQL，但其语义以 600 多页自然语言给出，难以形式推理与忠实实现。已有形式化或省略 bag 语义、schema 与多图复合查询，或只覆盖模式匹配等片段。本文提出 MGQL：GQL 只读子片段的首个机械化小步操作语义，直接以 ISO 标准为依据；它建模多图属性图与混合边方向，支持量化路径/边、有向与无向匹配、标签表达式、模式列表及复合查询。语义配有 schema 感知类型系统，用闭合图 schema 细化变量类型、跟踪可空性，并用列表类型建模量化路径绑定。作者证明该类型系统可靠，保证良构查询结果符合声明 schema，从而连接 GQL 的非形式规范与可执行实现。
Research and development of graph query languages has been gaining traction with the increase in popularity of graph databases, specifically due to the flexible schema and other rich semantic offerings of the latter’s most common underlying data model: the property graph. This has culminated in the standardization of the ISO Graph Query Language (GQL) as ISO/IEC 39075 in 2024, the first international standard for property graph- based graph query languages. However, ISO/IEC 39075 codifies its semantics informally across 600+ pages of prose, making it difficult to formally reason about the standard or for a standard-faithful implementation. Existing formalizations are not adequate because they either: (1) significantly reduce the semantic complexity by omitting bag semantics, schemas, and composite queries on multiple graphs; (2) or significantly reduce the syntactic complexity by only considering isolated fragments such as pattern-matching, leaving the full query pipeline unformalized. Yet it is these semantic–syntactic features that make formalizing GQL non-trivial. We present MGQL, the first mechanized, small-step operational semantics for a substantial read-only fragment of GQL that is grounded in the ISO/IEC 39075 standard. Our formalization models multi-graph property graphs with mixed edge directionality and supports a large fraction of GQL pattern constructs: quantified paths and edges, directional and undirected matching, label expressions, pattern lists, and composite queries. The semantics is supported by a schema-aware type system that refines variable types via closed-graph schemas, tracks nullability, supports multiple composite query operators, and models quantified-path bindings with list types. We prove that our type system is sound, ensuring an end-to-end guarantee of well-formed queries yielding results that conform to their declared schemas. MGQL provides the first bridge between GQL’s informal specification and a mechanized implementation, enabling formal reasoning about correctness.
@article{paperbot12100,
title = {MGQL: An Executable, Small-Step Semantics of GQL},
author = {Aditya Thimmaiah and Tong-Nong Lin and Milos Gligoric},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839459}
}