一句话：提出 TRAF：一种刻画 SQL 静态与动态类型及隐式类型转换的形式化类型语义框架，并给出类型安全条件与五引擎实例化验证。
实际 SQL 引擎在类型约束与隐式类型转换的处理上存在微妙差异，而这些差异通常被 SQL 的形式化研究忽略，直接影响查询在不同引擎间的可移植性。本文提出名为 TRAF 的 SQL 形式化类型语义，用抽象算子同时刻画静态与动态类型行为，从而能够系统性地建模 PostgreSQL、MS SQL Server、MySQL、SQLite 和 Oracle 等引擎的类型与转换行为。作者给出了该形式化体系对类型处理的形式化保证，识别出引擎实例化满足类型安全（type safety）与类型可靠性（type soundness）的实际条件，并指出 TRAF 可作为现有引擎类型行为可显式检验的刻画，指导其演进，并为类型感知查询优化与可证明正确的查询翻译器提供形式化基础。评估方面，作者用 Python 为五个引擎实现了 TRAF，并使用合成查询、SQLancer++ 生成的查询以及改造后的 Spider 与 Calcite 基准查询进行了充分性测试。
Practical SQL engines differ in subtle ways in their handling of typing constraints and implicit type casts. These issues, usually not considered in formal accounts of SQL, directly affect the portability of queries between engines. To address this problem, we present a formal typing semantics for SQL, named TRAF , that explicitly captures both static and dynamic type behavior. The system TRAF is expressed in terms of abstract operators that provide the necessary leeway to systematically model the type and cast behavior of different SQL engines (PostgreSQL, MS SQL Server, MySQL, SQLite, and Oracle). We show that this formalism provides formal guarantees for the handling of types. We identify practical conditions under which engine instantiations satisfy type safety and type soundness. In this regard, TRAF can serve as an explicit and testable account of typing in existing engines, potentially guide their evolution, and provide a formal basis to study type-aware query optimizations and design provably-correct query translators. We also test the adequacy of the formalism by implementing TRAF in Python for these five engines and testing it with synthetic queries, SQLancer++- generated queries, and adapted Spider and Calcite benchmark queries.
DOI 原文 ·
@inproceedings{paperbot3949,
title = {A Formal Framework for Typing and Cast Semantics in SQL Engines},
author = {Wenjia Ye and Matías Toro and Claudio Gutierrez and Bruno C. D. S. Oliveira and Éric Tanter},
booktitle = {TOPLAS},
year = {2026},
doi = {10.1145/3834861}
}