{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:10:54Z","timestamp":1746115854374,"version":"3.40.4"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031911170"},{"type":"electronic","value":"9783031911187"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"Abstract<\/jats:title>\n Practical SQL engines differ in subtle ways in their handling of typing constraints and implicit type casts. These issues, usually not considered in formal accounts\u00a0of SQL, directly affect the portability of queries between engines. To understand this problem, we present a formal typing semantics for SQL, named \n \n $$\\textsf{TRAF} $$<\/jats:tex-math>\n \n TRAF<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, that explicitly captures both static and dynamic type behavior. The system \n \n $$\\textsf{TRAF} $$<\/jats:tex-math>\n \n TRAF<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> is expressed in terms of abstract operators that provide the necessary leeway to precisely model different SQL engines (PostgreSQL, MS SQL Server, MySQL, SQLite, and Oracle).<\/jats:p>\n We show that this formalism provides formal guarantees regarding the handling of types. We provide practical conditions on engines to prove type safety and soundness of queries. In this regard, \n \n $$\\textsf{TRAF} $$<\/jats:tex-math>\n \n TRAF<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> can serve as precise documentation of typing in existing engines and potentially guide their evolution, as well as provide a formal basis to study type-aware query optimizations, and design provably-correct query translators. Additionally, we\u00a0test the adequacy of the formalism, implementing \n \n $$\\textsf{TRAF} $$<\/jats:tex-math>\n \n TRAF<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> in Python for these five engines, and tested them with thousands of randomly-generated queries.<\/jats:p>","DOI":"10.1007\/978-3-031-91118-7_16","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:07Z","timestamp":1746001027000},"page":"408-435","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Elucidating Type Conversions in SQL Engines"],"prefix":"10.1007","author":[{"given":"Wenjia","family":"Ye","sequence":"first","affiliation":[]},{"given":"Mat\u00edas","family":"Toro","sequence":"additional","affiliation":[]},{"given":"Claudio","family":"Gutierrez","sequence":"additional","affiliation":[]},{"given":"Bruno C. d. S.","family":"Oliveira","sequence":"additional","affiliation":[]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"16_CR1","unstructured":"Converting mysql to postgresql (2020), https:\/\/en.wikibooks.org\/wiki\/Converting_MySQL_to_PostgreSQL"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Ahadi, A., Behbood, V., Vihavainen, A., Prior, J., Lister, R.: Students\u2019 syntactic mistakes in writing seven different types of sql queries and its application to predicting students\u2019 success. In: Proceedings of the 47th ACM Technical Symposium on Computing Science Education. p. 401-406. SIGCSE \u201916, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2839509.2844640, https:\/\/doi.org\/10.1145\/2839509.2844640","DOI":"10.1145\/2839509.2844640"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Augustsson, L., \u00c5gren, M.: Experience report: Types for a relational algebra library. SIGPLAN Not. 51(12), 127-132 (sep 2016). https:\/\/doi.org\/10.1145\/3241625.2976016, https:\/\/doi.org\/10.1145\/3241625.2976016","DOI":"10.1145\/3241625.2976016"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Benzaken, V., Contejean, E.: A coq mechanised formal semantics for realistic sql queries: Formally reconciling sql and bag relational algebra. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. p. 249-261. CPP 2019, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3293880.3294107, https:\/\/doi.org\/10.1145\/3293880.3294107","DOI":"10.1145\/3293880.3294107"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Benzaken, V., Contejean, E., Hachmaoui, M.H., Keller, C., Mandel, L., Shinnar, A., Sim\u00e9on, J.: Translating canonical sql to imperative code in coq. Proc. ACM Program. Lang. 6(OOPSLA1) (apr 2022). https:\/\/doi.org\/10.1145\/3527327, https:\/\/doi.org\/10.1145\/3527327","DOI":"10.1145\/3527327"},{"key":"16_CR6","unstructured":"Bhandari, H., Chitrakar, R.: Comparison of data migration techniques from sql database to nosql database. J Comput Eng Inf Technol 9 6, \u00a02 (2020)"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Buneman, P., Ohori, A.: Polymorphism and type inference in database programming. ACM Trans. Database Syst. 21(1), 30-76 (mar 1996). https:\/\/doi.org\/10.1145\/227604.227609, https:\/\/doi.org\/10.1145\/227604.227609","DOI":"10.1145\/227604.227609"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Ceri, S., Gottlob, G.: Translating sql into relational algebra: Optimization, semantics, and equivalence of sql queries. IEEE Transactions on Software Engineering SE-11, 324\u2013345 (1985), https:\/\/api.semanticscholar.org\/CorpusID:22717180","DOI":"10.1109\/TSE.1985.232223"},{"key":"16_CR9","unstructured":"Chu, S., Wang, C., Weitz, K., Cheung, A.: Cosette: An automated prover for sql. In: Conference on Innovative Data Systems Research (2017), https:\/\/api.semanticscholar.org\/CorpusID:12408033"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Chu, S., Weitz, K., Cheung, A., Suciu, D.: Hottsql: proving query rewrites with univalent sql semantics. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (2016), https:\/\/api.semanticscholar.org\/CorpusID:644867","DOI":"10.1145\/3062341.3062348"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Colazzo, D., Sartiani, C.: Precision and complexity of xquery type inference. In: Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming. p. 89-100. PPDP \u201911, Association for Computing Machinery, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/2003476.2003490, https:\/\/doi.org\/10.1145\/2003476.2003490","DOI":"10.1145\/2003476.2003490"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Gaffney, K.P., Prammer, M., Brasfield, L.C., Hipp, D.R., Kennedy, D.R., Patel, J.M.: Sqlite: Past, present, and future. Proc. VLDB Endow. 15, 3535\u20133547 (2022), https:\/\/api.semanticscholar.org\/CorpusID:252066674","DOI":"10.14778\/3554821.3554842"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Gould, C., Su, Z., Devanbu, P.T.: JDBC checker: A static analysis tool for SQL\/JDBC applications. In: Finkelstein, A., Estublier, J., Rosenblum, D.S. (eds.) 26th International Conference on Software Engineering (ICSE 2004), 23-28 May 2004, Edinburgh, United Kingdom. pp. 697\u2013698. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/ICSE.2004.1317494, https:\/\/doi.org\/10.1109\/ICSE.2004.1317494","DOI":"10.1109\/ICSE.2004.1317494"},{"key":"16_CR14","unstructured":"Group, T.D.D.: Typechecking queries (2019), https:\/\/tpolecat.github.io\/doobie\/docs\/06-Checking.html"},{"key":"16_CR15","unstructured":"Group, T.K.D.: Kysely (2021), https:\/\/kysely.dev\/"},{"key":"16_CR16","unstructured":"Group, T.P.D.: Pgtyped (2020), https:\/\/github.com\/adelsz\/pgtyped"},{"key":"16_CR17","unstructured":"Group, T.P.G.D.: Postgresql documentation (1996), https:\/\/www.postgresql.org\/docs\/current\/typeconv-overview.html"},{"key":"16_CR18","unstructured":"Group, T.S.D.: Sqlines (2010), http:\/\/www.sqlines.com\/online"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Guagliardo, P., Libkin, L.: A formal semantics of sql queries, its validation, and applications. Proc. VLDB Endow. 11(1), 27-39 (sep 2017). https:\/\/doi.org\/10.14778\/3151113.3151116, https:\/\/doi.org\/10.14778\/3151113.3151116","DOI":"10.14778\/3151113.3151116"},{"key":"16_CR20","unstructured":"Haas, S.W.: Erik peter bansleben . database migration : A literature review and case study (2004), https:\/\/api.semanticscholar.org\/CorpusID:17518212"},{"key":"16_CR21","unstructured":"Hipp., D.R.: Most widely deployed and used database engine. https:\/\/www.sqlite.org\/mostdeployed.html"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Khan, S., Kalia, A., Dastjerdi, H.M., Nizamuddin, N.: Automated tool for nosql to sql migration. In: Proceedings of the 7th International Conference on Information Systems Engineering. p. 20-23. ICISE \u201922, Association for Computing Machinery, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3573926.3573931, https:\/\/doi.org\/10.1145\/3573926.3573931","DOI":"10.1145\/3573926.3573931"},{"key":"16_CR23","unstructured":"Lin, W.: Type inference in SQL. Ph.D. thesis, Concordia University (2004)"},{"key":"16_CR24","unstructured":"Marlow, S., et\u00a0al.: Haskell 2010 language report. Available online http:\/\/www.haskell.org\/(May 2011) (2010)"},{"key":"16_CR25","unstructured":"MIT: Ts-sql-query (2019), https:\/\/ts-sql-query.readthedocs.io\/"},{"key":"16_CR26","unstructured":"Necco, C.M., Nuno\u00a0Olivera, J.: Toward generic data processing. In: XI Congreso Argentino de Ciencias de la Computaci\u00f3n (2005)"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Negri, M., Pelagatti, G., Sbattella, L.: Formal semantics of sql queries. ACM Trans. Database Syst. 16(3), 513-534 (sep 1991). https:\/\/doi.org\/10.1145\/111197.111212, https:\/\/doi.org\/10.1145\/111197.111212","DOI":"10.1145\/111197.111212"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Ohori, A., Buneman, P.: Type inference in a database programming language. In: Proceedings of the 1988 ACM Conference on LISP and Functional Programming. p. 174-183. LFP \u201988, Association for Computing Machinery, New York, NY, USA (1988). https:\/\/doi.org\/10.1145\/62678.62700, https:\/\/doi.org\/10.1145\/62678.62700","DOI":"10.1145\/62678.62700"},{"key":"16_CR29","doi-asserted-by":"publisher","unstructured":"Park, D., Stefanescu, A., Rosu, G.: KJS: a complete formal semantics of javascript. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. pp. 346\u2013356. ACM (2015). https:\/\/doi.org\/10.1145\/2737924.2737991, https:\/\/doi.org\/10.1145\/2737924.2737991","DOI":"10.1145\/2737924.2737991"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Politz, J.G., Martinez, A., Milano, M., Warren, S., Patterson, D., Li, J., Chitipothu, A., Krishnamurthi, S.: Python: the full monty. In: Hosking, A.L., Eugster, P.T., Lopes, C.V. (eds.) Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013. pp. 217\u2013232. ACM (2013). https:\/\/doi.org\/10.1145\/2509136.2509536, https:\/\/doi.org\/10.1145\/2509136.2509536","DOI":"10.1145\/2509136.2509536"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"Ricciotti, W., Cheney, J.: A formalization of sql with nulls. J. Autom. Reason. 66(4), 989-1030 (nov 2022). https:\/\/doi.org\/10.1007\/s10817-022-09632-4, https:\/\/doi.org\/10.1007\/s10817-022-09632-4","DOI":"10.1007\/s10817-022-09632-4"},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"Silva, A., Visser, J.: Strong types for relational databases. In: Proceedings of the 2006 ACM SIGPLAN Workshop on Haskell. p. 25-36. Haskell \u201906, Association for Computing Machinery, New York, NY, USA (2006). https:\/\/doi.org\/10.1145\/1159842.1159846, https:\/\/doi.org\/10.1145\/1159842.1159846","DOI":"10.1145\/1159842.1159846"},{"key":"16_CR33","doi-asserted-by":"publisher","unstructured":"Smelcer, J.B.: User errors in database query composition. Int. J. Hum.-Comput. Stud. 42(4), 353-381 (apr 1995). https:\/\/doi.org\/10.1006\/ijhc.1995.1017, https:\/\/doi.org\/10.1006\/ijhc.1995.1017","DOI":"10.1006\/ijhc.1995.1017"},{"key":"16_CR34","doi-asserted-by":"publisher","unstructured":"Taipalus, T., Grahn, H., Ghanbari, H.: Error messages in relational database management systems: A comparison of effectiveness, usefulness, and user confidence. Journal of Systems and Software 181, 111034 (2021). https:\/\/doi.org\/10.1016\/j.jss.2021.111034, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S016412122100131X","DOI":"10.1016\/j.jss.2021.111034"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Taipalus, T., Siponen, M., Vartiainen, T.: Errors and complications in sql query formulation. ACM Trans. Comput. Educ. 18(3) (aug 2018). https:\/\/doi.org\/10.1145\/3231712, https:\/\/doi-org.eproxy.lib.hku.hk\/10.1145\/3231712","DOI":"10.1145\/3231712"},{"key":"16_CR36","doi-asserted-by":"publisher","unstructured":"Van den Bussche, J., Waller, E.: Polymorphic type inference for the relational algebra. Journal of Computer and System Sciences 64(3), 694\u2013718 (2002). https:\/\/doi.org\/10.1006\/jcss.2001.1812, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0022000001918124","DOI":"10.1006\/jcss.2001.1812"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Comprehending monads. Mathematical Structures in Computer Science 2, 461\u2013493 (1992)","DOI":"10.1017\/S0960129500001560"},{"key":"16_CR38","doi-asserted-by":"publisher","unstructured":"Wassermann, G., Gould, C., Su, Z., Devanbu, P.: Static checking of dynamically generated queries in database applications. ACM Trans. Softw. Eng. Methodol. 16(4), 14-es (sep 2007). https:\/\/doi.org\/10.1145\/1276933.1276935, https:\/\/doi.org\/10.1145\/1276933.1276935","DOI":"10.1145\/1276933.1276935"},{"key":"16_CR39","doi-asserted-by":"crossref","unstructured":"Welty, C.: Correcting user errors in sql. International Journal of Man-Machine Studies 22(4), 463\u2013477 (1985)","DOI":"10.1016\/S0020-7373(85)80051-1"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91118-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:25Z","timestamp":1746001045000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91118-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911170","9783031911187"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91118-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}