{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T02:20:28Z","timestamp":1785291628569,"version":"3.55.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>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 and query compilers to develop DBCert, the first mechanically verified compiler from SQL queries written in a canonical form to imperative code. Building DBCert required several new contributions which are described in this paper. First, we specify and mechanize a complete translation from SQL to the Nested Relational Algebra which can be used for query optimization. Second, we define Imp, a small imperative language sufficient to express SQL and which can target several execution languages including JavaScript. Finally, we develop a mechanized translation from the nested relational algebra to Imp, using the nested relational calculus as an intermediate step.<\/jats:p>","DOI":"10.1145\/3527327","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Translating canonical SQL to imperative code in Coq"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1227-3327","authenticated-orcid":false,"given":"V\u00e9ronique","family":"Benzaken","sequence":"first","affiliation":[{"name":"LMF, France \/ Universit\u00e9 Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8195-7861","authenticated-orcid":false,"given":"\u00c9velyne","family":"Contejean","sequence":"additional","affiliation":[{"name":"LMF, France \/ CNRS, France \/ Universit\u00e9 Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8030-807X","authenticated-orcid":false,"given":"Mohammed Houssem","family":"Hachmaoui","sequence":"additional","affiliation":[{"name":"LMF, France \/ Universit\u00e9 Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1282-0677","authenticated-orcid":false,"given":"Chantal","family":"Keller","sequence":"additional","affiliation":[{"name":"LMF, France \/ Universit\u00e9 Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5291-6067","authenticated-orcid":false,"given":"Louis","family":"Mandel","sequence":"additional","affiliation":[{"name":"IBM Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6259-0016","authenticated-orcid":false,"given":"Avraham","family":"Shinnar","sequence":"additional","affiliation":[{"name":"IBM Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8622-9716","authenticated-orcid":false,"given":"J\u00e9r\u00f4me","family":"Sim\u00e9on","sequence":"additional","affiliation":[{"name":"Docusign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Foundations of Databases","author":"Abiteboul Serge","unstructured":"Serge Abiteboul , Richard Hull , and Victor Vianu . 1995. Foundations of Databases . Addison-Wesley . Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of Databases. Addison-Wesley."},{"key":"e_1_2_1_2_1","unstructured":"2022. AlaSQL JavaScript SQL Database Library. http:\/\/alasql.org.  2022. AlaSQL JavaScript SQL Database Library. http:\/\/alasql.org."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3035961"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3056447"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294107"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6366579"},{"key":"e_1_2_1_7_1","volume-title":"Chantal Keller, Louis Mandel, Avraham Shinnar, and J\u00e9r\u00f4me Sim\u00e9on.","author":"Benzaken V\u00e9ronique","year":"2022","unstructured":"V\u00e9ronique Benzaken , \u00c9velyne Contejean , Mohammed Houssem Hachmaoui , Chantal Keller, Louis Mandel, Avraham Shinnar, and J\u00e9r\u00f4me Sim\u00e9on. 2022 . Translating Canonical SQL to Imperative Code in Coq \u2013 extended. CoRR , abs\/2203.08941 (2022), https:\/\/doi.org\/10.48550\/arXiv.2203.08941 10.48550\/arXiv.2203.08941 V\u00e9ronique Benzaken, \u00c9velyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and J\u00e9r\u00f4me Sim\u00e9on. 2022. Translating Canonical SQL to Imperative Code in Coq \u2013 extended. CoRR, abs\/2203.08941 (2022), https:\/\/doi.org\/10.48550\/arXiv.2203.08941"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375657.1375674"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1272743.1272748"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062348"},{"key":"e_1_2_1_12_1","volume-title":"Optimizing Queries with Universal Quantification in Object-Oriented and Object-Relational Databases. In Conference on Very Large Data Bases (VLDB). 286\u2013295","author":"Jens Clau\u00df","year":"1997","unstructured":"Jens Clau\u00df en, Alfons Kemper , Guido Moerkotte , and Klaus Peithner . 1997 . Optimizing Queries with Universal Quantification in Object-Oriented and Object-Relational Databases. In Conference on Very Large Data Bases (VLDB). 286\u2013295 . Jens Clau\u00df en, Alfons Kemper, Guido Moerkotte, and Klaus Peithner. 1997. Optimizing Queries with Universal Quantification in Object-Oriented and Object-Relational Databases. In Conference on Very Large Data Bases (VLDB). 286\u2013295."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.842265"},{"key":"e_1_2_1_14_1","volume-title":"Database Programming Languages (DBPL-4)","author":"Cluet Sophie","year":"1993","unstructured":"Sophie Cluet and Guido Moerkotte . 1993. Nested Queries in Object Bases . In Database Programming Languages (DBPL-4) , Manhattan, New York City, USA, 30 August - 1 September 1993 . 226\u2013242. Sophie Cluet and Guido Moerkotte. 1993. Nested Queries in Object Bases. In Database Programming Languages (DBPL-4), Manhattan, New York City, USA, 30 August - 1 September 1993. 226\u2013242."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1265530.1265535"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/BigData.2015.7364068"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.14778\/3151113.3151116"},{"key":"e_1_2_1_18_1","unstructured":"TU Jin-De. 2010. StreamSQL: A Query Language for Stream Data. Computer Systems & Applications 26.  TU Jin-De. 2010. StreamSQL: A Query Language for Stream Data. Computer Systems & Applications 26."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICITCS.2016.7740361"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"key":"e_1_2_1_22_1","unstructured":"Guido Moerkotte. 2020. Building Query Compilers. Univ. Mannheim. https:\/\/pi3.informatik.uni-mannheim.de\/~moer\/querycompiler.pdf  Guido Moerkotte. 2020. Building Query Compilers. Univ. Mannheim. https:\/\/pi3.informatik.uni-mannheim.de\/~moer\/querycompiler.pdf"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 2017 ACM International Conference on Management of Data, SIGMOD Conference 2017","year":"2017","unstructured":"2017. Proceedings of the 2017 ACM International Conference on Management of Data, SIGMOD Conference 2017 , Chicago, IL, USA , May 14-19, 2017 , Semih Salihoglu, Wenchao Zhou, Rada Chirkova, Jun Yang, and Dan Suciu (Eds.). ACM. isbn:978-1-4503-4197-4 http:\/\/dl.acm.org\/citation.cfm?id=3035918 2017. Proceedings of the 2017 ACM International Conference on Management of Data, SIGMOD Conference 2017, Chicago, IL, USA, May 14-19, 2017, Semih Salihoglu, Wenchao Zhou, Rada Chirkova, Jun Yang, and Dan Suciu (Eds.). ACM. isbn:978-1-4503-4197-4 http:\/\/dl.acm.org\/citation.cfm?id=3035918"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2882903.2915244"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2015.542"},{"key":"e_1_2_1_26_1","unstructured":"2021. SQL Alchemy: The Python SQL Toolkit and Object Relational Mapper. https:\/\/www.sqlalchemy.org.  2021. SQL Alchemy: The Python SQL Toolkit and Object Relational Mapper. https:\/\/www.sqlalchemy.org."},{"key":"e_1_2_1_27_1","unstructured":"2022. SQLite compiled to JavaScript. https:\/\/sql.js.org\/.  2022. SQLite compiled to JavaScript. https:\/\/sql.js.org\/."},{"key":"e_1_2_1_28_1","volume-title":"Principles of Database Systems","author":"Ullman Jeffrey D.","unstructured":"Jeffrey D. Ullman . 1982. Principles of Database Systems , 2 nd Edition. Computer Science Press . isbn:0-914894-36-6 Jeffrey D. Ullman. 1982. Principles of Database Systems, 2nd Edition. Computer Science Press. isbn:0-914894-36-6","edition":"2"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297661"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527327","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527327","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527327"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":29,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527327"],"URL":"https:\/\/doi.org\/10.1145\/3527327","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}