{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:25:25Z","timestamp":1784183125982,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":63,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,14]],"date-time":"2017-06-14T00:00:00Z","timestamp":1497398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-2-0032"],"award-info":[{"award-number":["FA8750-16-2-0032"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["IIS-1546083, IIS-1651489, III-1614738, AITF-1535565, CNS-1563788"],"award-info":[{"award-number":["IIS-1546083, IIS-1651489, III-1614738, AITF-1535565, CNS-1563788"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0016260"],"award-info":[{"award-number":["DE-SC0016260"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,6,14]]},"DOI":"10.1145\/3062341.3062348","type":"proceedings-article","created":{"date-parts":[[2017,6,14]],"date-time":"2017-06-14T10:01:04Z","timestamp":1497434464000},"page":"510-524","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":37,"title":["HoTTSQL: proving query rewrites with univalent SQL semantics"],"prefix":"10.1145","author":[{"given":"Shumo","family":"Chu","sequence":"first","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Konstantin","family":"Weitz","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alvin","family":"Cheung","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dan","family":"Suciu","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,6,14]]},"reference":[{"key":"e_1_3_2_1_1_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_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/6012.15399"},{"key":"e_1_3_2_1_3_1","unstructured":"B. Barras B. Gr\u00e9goire A. Mahboubi and L. Th\u00e9ry. Coq reference manual chapter 25: The ring and field tactic families. https:\/\/coq.inria.fr\/refman\/Reference-Manual028. html.  B. Barras B. Gr\u00e9goire A. Mahboubi and L. Th\u00e9ry. Coq reference manual chapter 25: The ring and field tactic families. https:\/\/coq.inria.fr\/refman\/Reference-Manual028. html."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_11"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/181550.181564"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00024-Q"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803397"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/248603.248616"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/153850.153856"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/182591.182604"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/233269.233356"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/276304.276311"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_2_1_16_1","volume-title":"HoTTSQL: Proving query rewrites with univalent SQL semantics. CoRR, abs\/1607.04822","author":"Chu S.","year":"2016","unstructured":"S. Chu , K. Weitz , A. Cheung , and D. Suciu . HoTTSQL: Proving query rewrites with univalent SQL semantics. CoRR, abs\/1607.04822 , 2016 . 04822. S. Chu, K. Weitz, A. Cheung, and D. Suciu. HoTTSQL: Proving query rewrites with univalent SQL semantics. CoRR, abs\/1607.04822, 2016. 04822."},{"key":"e_1_3_2_1_17_1","volume-title":"CIDR. www.cidrdb.org","author":"Chu S.","year":"2017","unstructured":"S. Chu , C. Wang , K. Weitz , and A. Cheung . Cosette: An automated prover for SQL . In CIDR. www.cidrdb.org , 2017 . S. Chu, C. Wang, K. Weitz, and A. Cheung. Cosette: An automated prover for SQL. In CIDR. www.cidrdb.org, 2017."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/362384.362685"},{"key":"e_1_3_2_1_19_1","volume-title":"R. Rustin (ed.): Database Systems: 65-98","author":"Codd E. F.","year":"1972","unstructured":"E. F. Codd . Relational completeness of data base sublanguages. In: R. Rustin (ed.): Database Systems: 65-98 , Prentice Hall and IBM Research Report RJ 987, San Jose, California, 1972 . E. F. Codd. Relational completeness of data base sublanguages. In: R. Rustin (ed.): Database Systems: 65-98, Prentice Hall and IBM Research Report RJ 987, San Jose, California, 1972."},{"key":"e_1_3_2_1_20_1","first-page":"341","volume-title":"VLDB","author":"Dar S.","unstructured":"S. Dar , M. J. Franklin , B. T. J\u00b4onsson , D. Srivastava , and M. Tan . Semantic data caching and replacement . In VLDB , pages 330\u2013 341 . Morgan Kaufmann, 1996. S. Dar, M. J. Franklin, B. T. J\u00b4onsson, D. Srivastava, and M. Tan. Semantic data caching and replacement. In VLDB, pages 330\u2013341. Morgan Kaufmann, 1996."},{"key":"e_1_3_2_1_21_1","volume-title":"C. J. Date. A Guide to the SQL Standard","year":"1989","unstructured":"C. J. Date. A Guide to the SQL Standard , Second Edition. Addison-Wesley , 1989 . ISBN 978-0-201-50209-1. C. J. Date. A Guide to the SQL Standard, Second Edition. Addison-Wesley, 1989. ISBN 978-0-201-50209-1."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/38713.38723"},{"key":"e_1_3_2_1_23_1","volume-title":"Database systems - the complete book (2. ed.). Pearson Education","author":"Garcia-Molina H.","year":"2009","unstructured":"H. Garcia-Molina , J. D. Ullman , and J. Widom . Database systems - the complete book (2. ed.). Pearson Education , 2009 . ISBN 978-0-13-187325-4. H. Garcia-Molina, J. D. Ullman, and J. Widom. Database systems - the complete book (2. ed.). Pearson Education, 2009. ISBN 978-0-13-187325-4."},{"key":"e_1_3_2_1_24_1","series-title":"LIPIcs","first-page":"17","volume-title":"ICDT","author":"Geck G.","unstructured":"G. Geck , B. Ketsman , F. Neven , and T. Schwentick . Parallelcorrectness and containment for conjunctive queries with union and negation . In ICDT , volume 48 of LIPIcs , pages 9:1\u2013 9: 17 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. G. Geck, B. Ketsman, F. Neven, and T. Schwentick. Parallelcorrectness and containment for conjunctive queries with union and negation. In ICDT, volume 48 of LIPIcs, pages 9:1\u2013 9:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016."},{"issue":"3","key":"e_1_3_2_1_25_1","first-page":"19","article-title":"The cascades framework for query optimization","volume":"18","author":"Graefe G.","year":"1995","unstructured":"G. Graefe . The cascades framework for query optimization . IEEE Data Eng. Bull. , 18 ( 3 ): 19 \u2013 29 , 1995 . G. Graefe. The cascades framework for query optimization. IEEE Data Eng. Bull., 18(3):19\u201329, 1995.","journal-title":"IEEE Data Eng. Bull."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/38713.38734"},{"key":"e_1_3_2_1_27_1","first-page":"218","volume-title":"ICDE","author":"Graefe G.","unstructured":"G. Graefe and W. J. McKenna . The volcano optimizer generator: Extensibility and efficient search . In ICDE , pages 209\u2013 218 . IEEE Computer Society, 1993. G. Graefe and W. J. McKenna. The volcano optimizer generator: Extensibility and efficient search. In ICDE, pages 209\u2013 218. IEEE Computer Society, 1993."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1265530.1265535"},{"key":"e_1_3_2_1_29_1","unstructured":"J. Gross M. Shulman A. Bauer P. L. Lumsdaine A. Mahboubi and B. Spitters. The hott libary in coq. https: \/\/github.com\/HoTT\/HoTT.  J. Gross M. Shulman A. Bauer P. L. Lumsdaine A. Mahboubi and B. Spitters. The hott libary in coq. https: \/\/github.com\/HoTT\/HoTT."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"Guttag J. V.","year":"1993","unstructured":"J. V. Guttag and J. J. Horning . Larch: Languages and Tools for Formal Specification . Springer-Verlag New York, Inc. , New York, NY, USA , 1993 . ISBN 0-387-94006-5. J. V. Guttag and J. J. Horning. Larch: Languages and Tools for Formal Specification. Springer-Verlag New York, Inc., New York, NY, USA, 1993. ISBN 0-387-94006-5."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/67544.66962"},{"key":"e_1_3_2_1_32_1","first-page":"181","volume-title":"OSDI","author":"Hawblitzel C.","unstructured":"C. Hawblitzel , J. Howell , J. R. Lorch , A. Narayan , B. Parno , D. Zhang , and B. Zill . Ironclad apps: End-to-end security via automated full-system verification . In OSDI , pages 165\u2013 181 . USENIX Association, 2014. C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad apps: End-to-end security via automated full-system verification. In OSDI, pages 165\u2013181. USENIX Association, 2014."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/211414.211419"},{"key":"e_1_3_2_1_34_1","volume-title":"https:\/\/www.iso.org\/obp\/ ui\/#iso:std:iso-iec:9075:-1:ed-4:v1:en. Online","author":"IEC.","year":"2016","unstructured":"ISO\/ IEC. Iso\/iec 9075-1:2011. https:\/\/www.iso.org\/obp\/ ui\/#iso:std:iso-iec:9075:-1:ed-4:v1:en. Online ; accessed 9- May - 2016 . ISO\/IEC. Iso\/iec 9075-1:2011. https:\/\/www.iso.org\/obp\/ ui\/#iso:std:iso-iec:9075:-1:ed-4:v1:en. Online; accessed 9-May-2016."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142363"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2902251.2902280"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_39_1","first-page":"107","volume-title":"VLDB","author":"Levy A. Y.","unstructured":"A. Y. Levy , I. S. Mumick , and Y. Sagiv . Query optimization by predicate move-around . In VLDB , pages 96\u2013 107 . Morgan Kaufmann, 1994. A. Y. Levy, I. S. Mumick, and Y. Sagiv. Query optimization by predicate move-around. In VLDB, pages 96\u2013107. Morgan Kaufmann, 1994."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815072.2815080"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/93597.98734"},{"key":"e_1_3_2_1_43_1","first-page":"102","volume-title":"VLDB","author":"Muralikrishna M.","unstructured":"M. Muralikrishna . Improved unnesting algorithms for join aggregate SQL queries . In VLDB , pages 91\u2013 102 . Morgan Kaufmann, 1992. M. Muralikrishna. Improved unnesting algorithms for join aggregate SQL queries. In VLDB, pages 91\u2013102. Morgan Kaufmann, 1992."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/111197.111212"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/130283.130294"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037407"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322221"},{"key":"e_1_3_2_1_49_1","unstructured":"D. Schmitt. Bug #5673: Optimizer creates strange execution plan leading to wrong results. https: \/\/www.postgresql.org\/message-id\/201009231503.  D. Schmitt. Bug #5673: Optimizer creates strange execution plan leading to wrong results. https: \/\/www.postgresql.org\/message-id\/201009231503."},{"key":"e_1_3_2_1_50_1","unstructured":"o8NF3Blt059661@wwwmaster.postgresql.org. Online; accessed 1-July-2016.  o8NF3Blt059661@wwwmaster.postgresql.org. Online; accessed 1-July-2016."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/233269.233360"},{"key":"e_1_3_2_1_52_1","unstructured":"M. Sulik. Bug #70038: Wrong select count distinct with a field included in two-column unique key. http:\/\/bugs.mysql. com\/bug.php?id=70038. Online; accessed 1-July-2016.  M. Sulik. Bug #70038: Wrong select count distinct with a field included in two-column unique key. http:\/\/bugs.mysql. com\/bug.php?id=70038. Online; accessed 1-July-2016."},{"key":"e_1_3_2_1_53_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program . Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book , Institute for Advanced Study , 2013 . The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book, Institute for Advanced Study, 2013."},{"issue":"1","key":"e_1_3_2_1_54_1","first-page":"569","article-title":"Impossibility of an algorithm for the decision problem in finite classes","volume":"70","author":"Trakhtenbrot B. A.","year":"1950","unstructured":"B. A. Trakhtenbrot . Impossibility of an algorithm for the decision problem in finite classes . Dok. Akad. Nauk USSR , 70 ( 1 ): 569 \u2013 572 , 1950 . B. A. Trakhtenbrot. Impossibility of an algorithm for the decision problem in finite classes. Dok. Akad. Nauk USSR, 70(1):569\u2013572, 1950.","journal-title":"Dok. Akad. Nauk USSR"},{"key":"e_1_3_2_1_55_1","unstructured":"Transaction Processing Performance Council (TPC). Tpc benchmark h revision 2.17.1. http:\/\/www.tpc.org\/tpc documents current versions\/pdf\/tpc-h v2.17.1.pdf.  Transaction Processing Performance Council (TPC). Tpc benchmark h revision 2.17.1. http:\/\/www.tpc.org\/tpc documents current versions\/pdf\/tpc-h v2.17.1.pdf."},{"key":"e_1_3_2_1_56_1","first-page":"378","volume-title":"VLDB","author":"Tsatalos O. G.","unstructured":"O. G. Tsatalos , M. H. Solomon , and Y. E. Ioannidis . The GMAP: A versatile tool for physical data independence . In VLDB , pages 367\u2013 378 . Morgan Kaufmann, 1994. O. G. Tsatalos, M. H. Solomon, and Y. E. Ioannidis. The GMAP: A versatile tool for physical data independence. In VLDB, pages 367\u2013378. Morgan Kaufmann, 1994."},{"key":"e_1_3_2_1_57_1","volume-title":"Principles of Database and Knowledge-Base Systems","author":"Ullman J. D.","year":"1989","unstructured":"J. D. Ullman . Principles of Database and Knowledge-Base Systems , Volume II. Computer Science Press , 1989 . J. D. Ullman. Principles of Database and Knowledge-Base Systems, Volume II. Computer Science Press, 1989."},{"key":"e_1_3_2_1_58_1","series-title":"Lecture Notes in Computer Science","first-page":"40","volume-title":"ICDT","author":"Ullman J. D.","unstructured":"J. D. Ullman . Information integration using logical views. In ICDT , volume 1186 of Lecture Notes in Computer Science , pages 19\u2013 40 . Springer, 1997. J. D. Ullman. Information integration using logical views. In ICDT, volume 1186 of Lecture Notes in Computer Science, pages 19\u201340. Springer, 1997."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/137097.137902"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_3"},{"key":"e_1_3_2_1_61_1","series-title":"Lecture Notes in Computer Science","first-page":"446","volume-title":"LPAR (Dakar)","author":"Veanes M.","unstructured":"M. Veanes , N. Tillmann , and J. de Halleux. Qex: Symbolic SQL query explorer . In LPAR (Dakar) , volume 6355 of Lecture Notes in Computer Science , pages 425\u2013 446 . Springer, 2010. M. Veanes, N. Tillmann, and J. de Halleux. Qex: Symbolic SQL query explorer. In LPAR (Dakar), volume 6355 of Lecture Notes in Computer Science, pages 425\u2013446. Springer, 2010."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"event":{"name":"PLDI '17: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Barcelona Spain","acronym":"PLDI '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3062341.3062348","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3062341.3062348","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3062341.3062348","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:32Z","timestamp":1750203392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3062341.3062348"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,14]]},"references-count":63,"alternative-id":["10.1145\/3062341.3062348","10.1145\/3062341"],"URL":"https:\/\/doi.org\/10.1145\/3062341.3062348","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3140587.3062348","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,6,14]]},"assertion":[{"value":"2017-06-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}