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.
Wed 25 OctDisplayed time zone: Lisbon change
16:00 - 17:48 | |||
16:00 18mTalk | Fluent APIs in Functional Languages OOPSLA DOI Pre-print | ||
16:18 18mTalk | A Pretty Expressive Printer OOPSLA Sorawee Porncharoenwase University of Washington, Justin Pombrio Unaffiliated, Emina Torlak Amazon Web Services, USA DOI Pre-print | ||
16:36 18mTalk | How Domain Experts Use an Embedded DSL OOPSLA Lisa Rennels University of California at Berkeley, Sarah E. Chasins University of California at Berkeley DOI | ||
16:54 18mTalk | Saggitarius: A DSL for Specifying Grammatical Domains OOPSLA Anders Miltner Simon Fraser University, Devon Loehr Princeton University, Arnold Mong Princeton University, Kathleen Fisher Tufts University, David Walker Princeton University DOI | ||
17:12 18mTalk | Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid OOPSLA Huanqi Cao Tsinghua University, Shizhi Tang Tsinghua University, Qianchao Zhu Peking University, Bowen Yu Tsinghua University, Wenguang Chen Tsinghua University; Pengcheng Laboratory DOI | ||
17:30 18mTalk | Translating canonical SQL to imperative code in Coq OOPSLA Véronique Benzaken Université Paris-Saclay - Laboratoire de Méthodes Formelles , Évelyne Contejean CNRS, ENS Paris-Saclay & Université Paris-Saclay, Houssem Hachmaoui , Chantal Keller Université Paris Saclay, Louis Mandel IBM Research, USA, Avraham Shinnar IBM Research, Jerome Simeon DocuSign, Inc. Link to publication DOI | ||