{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:18:58Z","timestamp":1770272338989,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DataCert ANR project,","award":["ANR-15-CE39-0009."],"award-info":[{"award-number":["ANR-15-CE39-0009."]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294107","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"249-261","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra"],"prefix":"10.1145","author":[{"given":"V\u00e9ronique","family":"Benzaken","sequence":"first","affiliation":[{"name":"University of Paris-Sud, France \/ LRI, France"}]},{"given":"\u00c9velyne","family":"Contejean","sequence":"additional","affiliation":[{"name":"CNRS, France \/ University of Paris-Sud, France \/ LRI, France"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"T. Arvin. 2017. Comparison of different SQL\u2019s implementations. http: \/\/troels.arvin.dk\/db\/rdbms  T. Arvin. 2017. Comparison of different SQL\u2019s implementations. http: \/\/troels.arvin.dk\/db\/rdbms"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3035961"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_11"},{"key":"e_1_3_2_1_4_1","volume-title":"International Conference on Interactive Theorem Proving (ITP 2018)","author":"Benzaken V.","unstructured":"V. Benzaken , \u00c9. Contejean, C. Keller , and E. Martins . 2018. A Coq formalisation of SQL\u2019s execution engines . In International Conference on Interactive Theorem Proving (ITP 2018) . Oxford, United Kingdom. V. Benzaken, \u00c9. Contejean, C. Keller, and E. Martins. 2018. A Coq formalisation of SQL\u2019s execution engines. In International Conference on Interactive Theorem Proving (ITP 2018) . Oxford, United Kingdom."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.232223"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062348"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"S. Cluet and G. 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.   S. Cluet and G. 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.","DOI":"10.1007\/978-1-4471-3564-7_13"},{"key":"e_1_3_2_1_8_1","unstructured":"H. Garcia-Molina J D. Ullman and J. Widom. 2009. Database systems -the complete book (2. ed.) . Pearson Education.   H. Garcia-Molina J D. Ullman and J. Widom. 2009. Database systems -the complete book (2. ed.) . Pearson Education."},{"key":"e_1_3_2_1_9_1","volume-title":"RelMiCS (LNCS)","author":"Gonzalia C.","unstructured":"C. Gonzalia . 2003. Towards a Formalisation of Relational Database Theory in Constructive Type Theory . In RelMiCS (LNCS) , R. Berghammer, B. M\u00f6ller, and G. Struth (Eds.), Vol. 3051 . Springer , 137\u2013148. C. Gonzalia. 2003. Towards a Formalisation of Relational Database Theory in Constructive Type Theory. In RelMiCS (LNCS), R. Berghammer, B. M\u00f6ller, and G. Struth (Eds.), Vol. 3051. Springer, 137\u2013148."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1265530.1265535"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.14778\/3151113.3151116"},{"key":"e_1_3_2_1_13_1","volume-title":"Practical Foundations for Programming Languages","author":"Harper R.","unstructured":"R. Harper . 2016. Practical Foundations for Programming Languages . Cambridge University Press . R. Harper. 2016. Practical Foundations for Programming Languages. Cambridge University Press."},{"key":"e_1_3_2_1_14_1","volume-title":"Information technology - Database Languages - SQL -Part 2: Foundation","author":"EC.","unstructured":"ISO\/I EC. 2006. Information technology - Database Languages - SQL -Part 2: Foundation (SQL\/Foundation). Final Commitee Draft . ISO\/IEC. 2006. Information technology - Database Languages - SQL -Part 2: Foundation (SQL\/Foundation). Final Commitee Draft."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/111197.111212"},{"key":"e_1_3_2_1_18_1","unstructured":"B. Pierce etal 2018. Software Foundations - Programming Languages Foundations . Vol. 2.  B. Pierce et al. 2018. Software Foundations - Programming Languages Foundations . Vol. 2."},{"key":"e_1_3_2_1_19_1","unstructured":"The Agda Development Team. 2010. The Agda Proof Assistant Reference Manual . http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php  The Agda Development Team. 2010. The Agda Proof Assistant Reference Manual . http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php"},{"key":"e_1_3_2_1_20_1","unstructured":"The Coq Development Team. 2010. The Coq Proof Assistant Reference Manual . http:\/\/coq.inria.fr  The Coq Development Team. 2010. The Coq Proof Assistant Reference Manual . http:\/\/coq.inria.fr"},{"key":"e_1_3_2_1_21_1","unstructured":"The Isabelle Development Team. 2010. The Isabelle Interactive Theorem Prover . https:\/\/isabelle.in.tum.de\/  The Isabelle Development Team. 2010. The Isabelle Interactive Theorem Prover . https:\/\/isabelle.in.tum.de\/"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Cascais Portugal","acronym":"CPP '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294107","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294107","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:50Z","timestamp":1750207430000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":20,"alternative-id":["10.1145\/3293880.3294107","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294107","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}