A Coq Formalisation of SQL's Execution Engines

Ch. Keller
Ch. Keller
E. Martins
E. Martins

ITP, pp. 88-107, 2018.

Cited by: 1|Bibtex|Views0|Links
EI

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments