{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:27Z","timestamp":1750219827941,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,6,18]],"date-time":"2023-06-18T00:00:00Z","timestamp":1687046400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DFG","award":["Project-ID~457292495"],"award-info":[{"award-number":["Project-ID~457292495"]}]},{"name":"EPSRC","award":["EP\/T022124\/1"],"award-info":[{"award-number":["EP\/T022124\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,6,18]]},"DOI":"10.1145\/3584372.3588653","type":"proceedings-article","created":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T22:21:22Z","timestamp":1685744482000},"page":"33-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Synthesizing Nested Relational Queries from Implicit Specifications"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2964-0880","authenticated-orcid":false,"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2964-0880","authenticated-orcid":false,"given":"C\u00e9cilia","family":"Pradic","sequence":"additional","affiliation":[{"name":"University of Swansea, Swansea, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2964-0880","authenticated-orcid":false,"given":"Christoph","family":"Wernhard","sequence":"additional","affiliation":[{"name":"University of Potsdam, Potsdam, Germany"}]}],"member":"320","published-online":{"date-parts":[[2023,6,18]]},"reference":[{"volume-title":"Answering Queries Using Views","author":"Afrati Foto","key":"e_1_3_2_1_1_1","unstructured":"Foto Afrati and Rada Chirkova. 2019. Answering Queries Using Views. Morgan & Claypool Publishers."},{"volume-title":"Intuitionistic set theory","author":"Bell John L.","key":"e_1_3_2_1_2_1","unstructured":"John L. Bell. 2014. Intuitionistic set theory. Vol. 50. College Publications London."},{"key":"e_1_3_2_1_3_1","volume-title":"Log. Methods Comput. Sci.","volume":"15","author":"Benedikt Michael","year":"2019","unstructured":"Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. 2019. Definability and Interpolation within Decidable Fixpoint Logics. Log. Methods Comput. Sci. , Vol. 15, 3 (2019), 29:1--29:53."},{"key":"e_1_3_2_1_4_1","volume-title":"Julien Leblay, and Efthymia Tsamoura.","author":"Benedikt Michael","year":"2016","unstructured":"Michael Benedikt, Balden Ten Cate, Julien Leblay, and Efthymia Tsamoura. 2016a. Generating Plans from Proofs: The Interpolation-Based Approach to Query Reformulation. Morgan Claypool."},{"key":"e_1_3_2_1_5_1","volume-title":"Reformulating Queries: Theory and Practice. In IJCAI.","author":"Benedikt Michael","year":"2017","unstructured":"Michael Benedikt, Egor V. Kostylev, Fabio Mogavero, and Efthymia Tsamoura. 2017. Reformulating Queries: Theory and Practice. In IJCAI."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Michael Benedikt and C\u00e9cilia Pradic. 2021. Generating Collection Transformations from Proofs. In POPL.","DOI":"10.1145\/3434295"},{"key":"e_1_3_2_1_7_1","volume-title":"Balder ten Cate, and Michael Vanden Boom","author":"Benedikt Michael","year":"2016","unstructured":"Michael Benedikt, Balder ten Cate, and Michael Vanden Boom. 2016b. Effective Interpolation and Preservation in Guarded Logics. ACM TOCL, Vol. 17, 2 (2016), 8:1--8:46."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1385-7258(53)50042-3"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1964-11244-1"},{"key":"e_1_3_2_1_10_1","unstructured":"C. C. Chang and H. Jerome Keisler. 1992. Model Theory. North-Holland."},{"key":"e_1_3_2_1_11_1","first-page":"250","article-title":"a","volume":"22","author":"Craig William","year":"1957","unstructured":"William Craig. 1957 a. Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem. J. Symb. Log. , Vol. 22, 03 (1957), 250--268.","journal-title":"Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem. J. Symb. Log."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586539"},{"volume-title":"First-order Logic and Automated Theorem Proving","author":"Fitting Melvin","key":"e_1_3_2_1_14_1","unstructured":"Melvin Fitting. 1996. First-order Logic and Automated Theorem Proving second ed.). Springer."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591248.2591269"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1090\/pspum\/025\/9940"},{"key":"e_1_3_2_1_17_1","volume-title":"Logique et Analyse","volume":"18","author":"Hodges Wilfrid","year":"1975","unstructured":"Wilfrid Hodges. 1975. A Normal Form for Algebraic Constructions II. Logique et Analyse, Vol. 18, 71\/72 (1975), 429--487."},{"volume-title":"Model Theory","author":"Hodges Wilfrid","key":"e_1_3_2_1_18_1","unstructured":"Wilfrid Hodges. 1993. Model Theory. Cambridge University Press."},{"key":"e_1_3_2_1_19_1","first-page":"169","article-title":"Omega-Categoricity","volume":"46","author":"Hodges Wilfrid","year":"1990","unstructured":"Wilfrid Hodges, I.M. Hodkinson, and Dugald Macpherson. 1990. Omega-Categoricity, Relative Categoricity and Coordinatisation. APAL, Vol. 46, 2 (1990), 169 -- 199.","journal-title":"Relative Categoricity and Coordinatisation. APAL"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Eva Hoogland Maarten Marx and Martin Otto. 1999. Beth Definability for the Guarded Fragment. In LPAR.","DOI":"10.1007\/3-540-48242-3_17"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Guoxiang Huang. 1995. Constructing Craig Interpolation Formulas. In Computing and Combinatorics.","DOI":"10.1007\/BFb0030832"},{"volume-title":"Set Theory","author":"Jech Thomas","key":"e_1_3_2_1_22_1","unstructured":"Thomas Jech. 2003. Set Theory. Springer."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189769.1189771"},{"key":"e_1_3_2_1_24_1","unstructured":"Phokion G. Kolaitis. 1990. Implicit Definability on Finite Structures and Unambiguous Computations. In LICS."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(70)90003-3"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Jaroslaw Kwiecien Jerzy Marcinkowski and Piotr Ostropolski-Nalewaja. 2022. Determinacy of Real Conjunctive Queries. The Boolean Case. In PODS.","DOI":"10.1145\/3517804.3524168"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1959.9.129"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01897040"},{"key":"e_1_3_2_1_29_1","first-page":"103091","article-title":"From Axioms to Synthetic Inference Rules via Focusing","volume":"173","author":"Marin Sonia","year":"2022","unstructured":"Sonia Marin, Dale Miller, Elaine Pimentel, and Marco Volpe. 2022. From Axioms to Synthetic Inference Rules via Focusing. APAL, Vol. 173, 5 (2022), 103091.","journal-title":"APAL"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806907.1806913"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.2307\/420966"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/128765.128768"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Luc Segoufin and Victor Vianu. 2005. Views and Queries: Determinacy and Rewriting. In PODS.","DOI":"10.1145\/1065167.1065174"},{"volume-title":"Craig's Interpolation Lemma and Beth's Definability Theorem. textnormalIn: First-Order Logic","author":"Smullyan Raymond M.","key":"e_1_3_2_1_34_1","unstructured":"Raymond M. Smullyan. 1968. Craig's Interpolation Lemma and Beth's Definability Theorem. textnormalIn: First-Order Logic. Springer, 127--133."},{"key":"e_1_3_2_1_35_1","unstructured":"Dan Suciu. 1995. Parallel Programming Languages for Collections. Ph. D. Dissertation. Univ. Pennsylvania."},{"volume-title":"Proof Theory","author":"Takeuti Gaisi","key":"e_1_3_2_1_36_1","unstructured":"Gaisi Takeuti. 1987. Proof Theory second ed.). North-Holland."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.4057"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"David Toman and Grant Weddell. 2011. Fundamentals of Physical Design and Query Compilation. Morgan Claypool.","DOI":"10.1007\/978-3-031-01881-7"},{"key":"e_1_3_2_1_39_1","volume-title":"Troelstra and Helmut Schwichtenberg","author":"Arne","year":"2000","unstructured":"Arne S. Troelstra and Helmut Schwichtenberg. 2000. Basic Proof Theory. Cambridge University Press."},{"key":"e_1_3_2_1_40_1","first-page":"1","article-title":"Simulation of the Nested Relational Algebra by the Flat Relational Algebra, with an Application to the Complexity of Evaluating Powerset Algebra Expressions","volume":"254","author":"den Bussche Jan Van","year":"2001","unstructured":"Jan Van den Bussche. 2001. Simulation of the Nested Relational Algebra by the Flat Relational Algebra, with an Application to the Complexity of Evaluating Powerset Algebra Expressions. Theor. Comput. Sci. , Vol. 254, 1--2 (2001), 363--377.","journal-title":"Theor. Comput. Sci."},{"key":"e_1_3_2_1_41_1","unstructured":"Limsoon Wong. 1994. Querying Nested Collections. Ph. D. Dissertation. Univ. Pennsylvania. iograp"}],"event":{"name":"SIGMOD\/PODS '23: International Conference on Management of Data","sponsor":["SIGMOD ACM Special Interest Group on Management of Data"],"location":"Seattle WA USA","acronym":"SIGMOD\/PODS '23"},"container-title":["Proceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3584372.3588653","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3584372.3588653","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:28Z","timestamp":1750178788000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3584372.3588653"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,18]]},"references-count":41,"alternative-id":["10.1145\/3584372.3588653","10.1145\/3584372"],"URL":"https:\/\/doi.org\/10.1145\/3584372.3588653","relation":{},"subject":[],"published":{"date-parts":[[2023,6,18]]},"assertion":[{"value":"2023-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}