A Coq Formalisation of SQL's Execution Engines
ITP, pp. 88-107, 2018.
In this article, we use the Coq proof assistant to specify and verify the low level layer of SQL’s execution engines. To reach our goals, we first design a high-level Coq specification for data-centric operators intended to capture their essence. We, then, provide two Coq implementations of our specification. The first one, the physical a...More
Full Text (Upload PDF)
PPT (Upload PPT)