Translating Canonical SQL to Imperative Code in Coq

Autor: Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2022, 6 (OOPSLA1), pp.1-27. ⟨10.1145/3527327⟩

SQL is by far the most widely used and implemented query language. Yet, on some key features, such as correlated queries and NULL value semantics, many implementations diverge or contain bugs. We leverage recent advances in the formalization of SQL a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::58e08a0905f3fec0e939cb78aeecd529

A Coq mechanised formal semantics for realistic SQL queries : Formally reconciling SQL and (extended) relational algebra

Autor: Véronique Benzaken, Evelyne Contejean

Publikováno v: EasyChair Preprints.

In this article, we provide a Coq mechanised, executable, formal semantics for realistic SQL queries consisting of select [distinct] from where group by having queries with NULL values, functions, aggregates, quantifiers and nested, potentially corre

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::de10ec9a6d20c7feeb0ff1747abd4790
https://doi.org/10.29007/dzdg

A Coq formalisation of SQL's execution engines

Autor: Eunice Martins, Véronique Benzaken, Chantal Keller, Evelyne Contejean

Publikováno v: ITP 2018: Interactive Theorem Proving
ITP 2018-International Conference on Interactive Theorem Proving
ITP 2018-International Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.88-107, ⟨10.1007/978-3-319-94821-8_6⟩
Interactive Theorem Proving ISBN: 9783319948201
ITP

International audience; 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 ca

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0bd7d34963ccd92e7c3073631bc6d026
https://hal.archives-ouvertes.fr/hal-01716048/file/main.pdf

Language-Integrated Queries

Autor: Giuseppe Castagna, Laurent Daynès, Véronique Benzaken, Romain Vernoux, Kim Nguyen, Julien Lopez

Publikováno v: WWW (Companion Volume)
WWW 2018-International World Wide Web Conference
WWW 2018-International World Wide Web Conference, Apr 2018, Lyon, France. pp.1-16, ⟨10.1145/3184558.3185973⟩

International audience; We present BOLDR, a modular framework that enables the evaluation in databases of queries containing application logic and, in particular, user-defined functions. BOLDR also allows the nesting of queries for different database

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ff14c772168fe2900146ed4c418ca639
https://doi.org/10.1145/3184558.3185973

Static and dynamic semantics of NoSQL languages

Autor: Jérôme Siméon, Kim Nguy ~ên, Giuseppe Castagna, Véronique Benzaken

Publikováno v: POPL
POPL, Jan 2013, Rome, Italy. pp.101-114, ⟨10.1145/2429069.2429083⟩

International audience; We present a calculus for processing semistructured data that spans differences of application area among several novel query languages, broadly categorized as ''NoSQL''. This calculus lets users define their own operators, ca

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::27799f1b52a83638536b7f321582ee96
https://doi.org/10.1145/2480359.2429083