{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T04:45:57Z","timestamp":1791089157350,"version":"4.1.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. VLDB Endow."],"published-print":{"date-parts":[[2017,9]]},"abstract":"<jats:p>While formal semantics of theoretical languages underlying SQL have been provided in the past, they all made simplifying assumptions ranging from changes in the syntax to omitting bag semantics and nulls. This situation is reminiscent of what happens in the field of programming languages, where semantics of formal calculi underlying the main features of languages are abundant, but formal semantics of real languages that people use are few and far between.<\/jats:p>\n          <jats:p>\n            We consider the basic class of SQL queries --- essentially\n            <jats:bold>SELECT-FROM-WHERE<\/jats:bold>\n            queries with subqueries, set\/bag operations, and nulls --- and define a formal semantics for it, without any departures from the real language. This fragment already requires decisions related to the data model and handling variable names that are normally disregarded by simplified semantics. To justify our choice of the semantics, we validate it experimentally on a large number of randomly generated queries and databases.\n          <\/jats:p>\n          <jats:p>We give two applications of the semantics. One is the first formal proof of the equivalence of basic SQL and relational algebra that extends to bag semantics and nulls. The other application looks at the three-valued logic employed by SQL, which is universally assumed to be necessary to handle nulls. We prove however that this is not so, as three-valued logic does not add expressive power: every SQL query in our fragment can be evaluated under the usual two-valued Boolean semantics of conditions.<\/jats:p>","DOI":"10.14778\/3151113.3151116","type":"journal-article","created":{"date-parts":[[2017,10,19]],"date-time":"2017-10-19T12:30:08Z","timestamp":1508416208000},"page":"27-39","source":"Crossref","is-referenced-by-count":42,"title":["A formal semantics of SQL queries, its validation, and applications"],"prefix":"10.14778","volume":"11","author":[{"given":"Paolo","family":"Guagliardo","sequence":"first","affiliation":[{"name":"University of Edinburgh"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leonid","family":"Libkin","sequence":"additional","affiliation":[{"name":"University of Edinburgh"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010051815785"},{"key":"e_1_2_1_2_1","volume-title":"Foundations of Databases","author":"Abiteboul S.","year":"1995","unstructured":"S. Abiteboul , R. Hull , and V. Vianu . Foundations of Databases . Addison-Wesley , 1995 . S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/645917.672310"},{"key":"e_1_2_1_4_1","unstructured":"T. Arvin. Comparison of different SQL implementations. http:\/\/troels.arvin.dk\/db\/rdbms 2017.  T. Arvin. Comparison of different SQL implementations. http:\/\/troels.arvin.dk\/db\/rdbms 2017."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841600017X"},{"key":"e_1_2_1_6_1","volume-title":"Many-Valued Logics: Theoretical Foundations","author":"Bolk L.","year":"1992","unstructured":"L. Bolk and P. Borowik . Many-Valued Logics: Theoretical Foundations . Springer , 1992 . L. Bolk and P. Borowik. Many-Valued Logics: Theoretical Foundations. Springer, 1992."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.232223"},{"key":"e_1_2_1_8_1","volume-title":"CIDR","author":"Chu S.","year":"2017","unstructured":"S. Chu , C. Wang , K. Weitz , and A. Cheung . Cosette: An automated prover for SQL . In CIDR , 2017 . S. Chu, C. Wang, K. Weitz, and A. Cheung. Cosette: An automated prover for SQL. In CIDR, 2017."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062348"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.842265"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1734714.1734718"},{"key":"e_1_2_1_12_1","unstructured":"F. Coelho. DataFiller --- generate random data from database schema. https:\/\/www.cri.ensmp.fr\/people\/coelho\/datafiller.html.  F. Coelho. DataFiller --- generate random data from database schema. https:\/\/www.cri.ensmp.fr\/people\/coelho\/datafiller.html."},{"key":"e_1_2_1_13_1","volume-title":"A Guide to the SQL Standard","author":"Date C. J.","year":"1996","unstructured":"C. J. Date and H. Darwen . A Guide to the SQL Standard . Addison-Wesley , 1996 . C. J. Date and H. Darwen. A Guide to the SQL Standard. Addison-Wesley, 1996."},{"key":"e_1_2_1_15_1","volume-title":"Pearson Education","author":"Garcia-Molina H.","year":"2009","unstructured":"H. Garcia-Molina , J. D. Ullman , and J. Widom . Database Systems - The Complete Book . Pearson Education , 2009 . H. Garcia-Molina, J. D. Ullman, and J. Widom. Database Systems - The Complete Book. Pearson Education, 2009."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1996.0042"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2902251.2902297"},{"key":"e_1_2_1_18_1","volume-title":"Semantics of Programming Languages: Structures and Techniques","author":"Gunter C.","year":"1992","unstructured":"C. Gunter . Semantics of Programming Languages: Structures and Techniques . MIT Press , 1992 . C. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992."},{"key":"e_1_2_1_19_1","first-page":"274","volume-title":"6th Workshop, CSL '92","author":"Gurevich Y.","year":"1992","unstructured":"Y. Gurevich and J. K. Huggins . The semantics of the C programming language. In Computer Science Logic , 6th Workshop, CSL '92 , pages 274 -- 308 , 1992 . Y. Gurevich and J. K. Huggins. The semantics of the C programming language. In Computer Science Logic, 6th Workshop, CSL '92, pages 274--308, 1992."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781316576892","volume-title":"Practical Foundations for Programming Languages","author":"Harper R.","year":"2016","unstructured":"R. Harper . Practical Foundations for Programming Languages . Cambridge University Press , 2016 . R. Harper. Practical Foundations for Programming Languages. Cambridge University Press, 2016."},{"key":"e_1_2_1_21_1","volume-title":"Information technology --- Database languages --- SQL","author":"International Organization for Standardization. ISO\/IEC 9075:2016","year":"2016","unstructured":"International Organization for Standardization. ISO\/IEC 9075:2016 : Information technology --- Database languages --- SQL , 2016 . International Organization for Standardization. ISO\/IEC 9075:2016: Information technology --- Database languages --- SQL, 2016."},{"key":"e_1_2_1_22_1","volume-title":"SQL in a Nutshell. O'Reilly & Associates","author":"Kline K. E.","year":"2001","unstructured":"K. E. Kline and D. Kline . SQL in a Nutshell. O'Reilly & Associates , Inc ., 2001 . K. E. Kline and D. Kline. SQL in a Nutshell. O'Reilly & Associates, Inc., 2001."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1997.1523"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"key":"e_1_2_1_25_1","first-page":"13","volume-title":"Handbook of the History of Logic","author":"Malinowski G.","year":"2007","unstructured":"G. Malinowski . Many-valued logic and its philosophy . In Handbook of the History of Logic , pages 13 -- 94 . Elsevier , 2007 . G. Malinowski. Many-valued logic and its philosophy. In Handbook of the History of Logic, pages 13--94. Elsevier, 2007."},{"key":"e_1_2_1_26_1","volume-title":"Commentary on standard ML","author":"Milner R.","year":"1991","unstructured":"R. Milner and M. Tofte . Commentary on standard ML . MIT Press , 1991 . R. Milner and M. Tofte. Commentary on standard ML. MIT Press, 1991."},{"key":"e_1_2_1_27_1","volume-title":"Definition of standard ML","author":"Milner R.","year":"1990","unstructured":"R. Milner , M. Tofte , and R. Harper . Definition of standard ML . MIT Press , 1990 . R. Milner, M. Tofte, and R. Harper. Definition of standard ML. MIT Press, 1990."},{"key":"e_1_2_1_28_1","volume-title":"Concepts in programming languages","author":"Mitchell J. C.","year":"2003","unstructured":"J. C. Mitchell . Concepts in programming languages . Cambridge University Press , 2003 . J. C. Mitchell. Concepts in programming languages. Cambridge University Press, 2003."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/111197.111212"},{"key":"e_1_2_1_30_1","unstructured":"Neo Technlogy Inc. openCypher project http:\/\/www.opencypher.org\/.  Neo Technlogy Inc. openCypher project http:\/\/www.opencypher.org\/."},{"key":"e_1_2_1_31_1","volume-title":"C formalised in HOL. Univ","author":"Norrish M.","year":"1998","unstructured":"M. Norrish . C formalised in HOL. Univ . Cambridge Techreport UCAM-CL-TR- 453, 150pp., 1998 . M. Norrish. C formalised in HOL. Univ. Cambridge Techreport UCAM-CL-TR- 453, 150pp., 1998."},{"key":"e_1_2_1_33_1","volume-title":"Database Management Systems","author":"Ramakrishnan R.","year":"2003","unstructured":"R. Ramakrishnan and J. Gehrke . Database Management Systems . McGraw-Hill , 2003 . R. Ramakrishnan and J. Gehrke. Database Management Systems. McGraw-Hill, 2003."},{"key":"e_1_2_1_34_1","volume-title":"Reidel","author":"Rescher N.","year":"1969","unstructured":"N. Rescher . Topics in Philosophical Logic . Reidel , 1969 . N. Rescher. Topics in Philosophical Logic. Reidel, 1969."},{"key":"e_1_2_1_35_1","volume-title":"TPC Benchmark\u2122 H Standard Specification","author":"Transaction Processing Performance Council","year":"2014","unstructured":"Transaction Processing Performance Council . TPC Benchmark\u2122 H Standard Specification , 2014 . Revision 2.17.1. Transaction Processing Performance Council. TPC Benchmark\u2122 H Standard Specification, 2014. Revision 2.17.1."},{"key":"e_1_2_1_36_1","volume-title":"Hasselt University and Universit\u00e9 Libre de Bruxelles","author":"Van den Bussche J.","year":"2009","unstructured":"J. Van den Bussche and S. Vansummeren . Translating SQL into the relational algebra. Course notes , Hasselt University and Universit\u00e9 Libre de Bruxelles , 2009 . J. Van den Bussche and S. Vansummeren. Translating SQL into the relational algebra. Course notes, Hasselt University and Universit\u00e9 Libre de Bruxelles, 2009."},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-642-17511-4_24","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"Veanes M.","year":"2010","unstructured":"M. Veanes , N. Tillmann , and J. de Halleux. Qex: Symbolic SQL query explorer . In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) , pages 425 -- 446 , 2010 . M. Veanes, N. Tillmann, and J. de Halleux. Qex: Symbolic SQL query explorer. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pages 425--446, 2010."}],"container-title":["Proceedings of the VLDB Endowment"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.14778\/3151113.3151116","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:33:57Z","timestamp":1672223637000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.14778\/3151113.3151116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["10.14778\/3151113.3151116"],"URL":"https:\/\/doi.org\/10.14778\/3151113.3151116","relation":{},"ISSN":["2150-8097"],"issn-type":[{"value":"2150-8097","type":"print"}],"subject":[],"published":{"date-parts":[[2017,9]]}}}