{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T20:26:32Z","timestamp":1768422392076,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,1,20]],"date-time":"2020-01-20T00:00:00Z","timestamp":1579478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,1,20]]},"DOI":"10.1145\/3372885.3373822","type":"proceedings-article","created":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T13:09:33Z","timestamp":1579698573000},"page":"201-214","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A mechanized formalization of GraphQL"],"prefix":"10.1145","author":[{"given":"Tom\u00e1s","family":"D\u00edaz","sequence":"first","affiliation":[{"name":"IMFD, Chile"}]},{"given":"Federico","family":"Olmedo","sequence":"additional","affiliation":[{"name":"University of Chile, Chile \/ IMFD, Chile"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile \/ IMFD, Chile \/ Inria, France"}]}],"member":"320","published-online":{"date-parts":[[2020,1,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3056447"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294107"},{"key":"e_1_3_2_1_3_1","first-page":"208","volume-title":"ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014","author":"Benzaken V.","year":"2014","unstructured":"Benzaken , V. , Contejean , E. , and Dumbrava , S . A Coq formalization of the relational data model. In Programming Languages and Systems - 23rd European Symposium on Programming , ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014 , Proceedings ( 2014 ), pp. 189\u2013 208 . Benzaken, V., Contejean, E., and Dumbrava, S. A Coq formalization of the relational data model. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (2014), pp. 189\u2013208."},{"key":"e_1_3_2_1_4_1","first-page":"188","volume-title":"ITP 2017, Bras\u00edlia, Brazil, September 26-29, 2017","author":"Benzaken V.","year":"2017","unstructured":"Benzaken , V. , Contejean , E. , and Dumbrava , S . Certifying standard and stratified Datalog inference engines in Ssreflect. In Interactive Theorem Proving - 8th International Conference , ITP 2017, Bras\u00edlia, Brazil, September 26-29, 2017 , Proceedings ( 2017 ), pp. 171\u2013 188 . Benzaken, V., Contejean, E., and Dumbrava, S. Certifying standard and stratified Datalog inference engines in Ssreflect. In Interactive Theorem Proving - 8th International Conference, ITP 2017, Bras\u00edlia, Brazil, September 26-29, 2017, Proceedings (2017), pp. 171\u2013188."},{"key":"e_1_3_2_1_5_1","first-page":"107","volume-title":"9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018","author":"Benzaken V.","year":"2018","unstructured":"Benzaken , V. , Contejean , E. , Keller , C. , and Martins , E . A Coq formalisation of SQL\u2019s execution engines. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018 , Proceedings ( 2018 ), pp. 88\u2013 107 . Benzaken, V., Contejean, E., Keller, C., and Martins, E. A Coq formalisation of SQL\u2019s execution engines. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (2018), pp. 88\u2013107."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276945.3276946"},{"key":"e_1_3_2_1_8_1","first-page":"3","article-title":"Certified graph view maintenance with regular Datalog","volume":"18","author":"Bonifati A.","year":"2018","unstructured":"Bonifati , A. , Dumbrava , S. , and Arias , E. J. G. Certified graph view maintenance with regular Datalog . TPLP 18 , 3 - 4 ( 2018 ), 372\u2013389. Bonifati, A., Dumbrava, S., and Arias, E. J. G. Certified graph view maintenance with regular Datalog. TPLP 18, 3-4 (2018), 372\u2013389.","journal-title":"TPLP"},{"key":"e_1_3_2_1_9_1","volume-title":"Schema validation and evolution for graph databases. CoRR abs\/1902.06427","author":"Bonifati A.","year":"2019","unstructured":"Bonifati , A. , Furniss , P. , Green , A. , Harmer , R. , Oshurko , E. , and Voigt , H . Schema validation and evolution for graph databases. CoRR abs\/1902.06427 ( 2019 ). Bonifati, A., Furniss, P., Green, A., Harmer, R., Oshurko, E., and Voigt, H. Schema validation and evolution for graph databases. CoRR abs\/1902.06427 (2019)."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/BigData.2017.8258173"},{"key":"e_1_3_2_1_11_1","first-page":"11","article-title":"Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries","volume":"11","author":"Chu S.","year":"2018","unstructured":"Chu , S. , Cheung , A. , and Suciu , D . Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries . Proceedings of VLDB 11 , 11 ( 2018 ), 1482\u20131495. Chu, S., Cheung, A., and Suciu, D. Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries. Proceedings of VLDB 11 , 11 (2018), 1482\u20131495.","journal-title":"Proceedings of VLDB"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062348"},{"key":"e_1_3_2_1_13_1","volume-title":"May","author":"Doczkal C.","year":"2019","unstructured":"Doczkal , C. , and Pous , D . Graph theory in Coq: Minors, treewidth, and isomorphisms , May 2019 . Available at https:\/\/hal.archivesouvertes.fr\/hal- 02127698 . Doczkal, C., and Pous, D. Graph theory in Coq: Minors, treewidth, and isomorphisms, May 2019. Available at https:\/\/hal.archivesouvertes.fr\/hal- 02127698 ."},{"key":"e_1_3_2_1_15_1","volume-title":"GraphQL specification. https:\/\/graphql. github.io\/graphql- spec\/June2018\/","author":"Graph QL","year":"2018","unstructured":"Graph QL Foundation . GraphQL specification. https:\/\/graphql. github.io\/graphql- spec\/June2018\/ , 2018 . GraphQL Foundation. GraphQL specification. https:\/\/graphql. github.io\/graphql- spec\/June2018\/ , 2018."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3327964.3328495"},{"key":"e_1_3_2_1_17_1","first-page":"1164","volume-title":"Proceedings of the 2018 World Wide Web Conference (Republic and Canton of Geneva, Switzerland, 2018), WWW \u201918, International World Wide Web Conferences Steering Committee","author":"Hartig O.","unstructured":"Hartig , O. , and P\u00e9rez , J . Semantics and complexity of GraphQL . In Proceedings of the 2018 World Wide Web Conference (Republic and Canton of Geneva, Switzerland, 2018), WWW \u201918, International World Wide Web Conferences Steering Committee , pp. 1155\u2013 1164 . Hartig, O., and P\u00e9rez, J. Semantics and complexity of GraphQL. In Proceedings of the 2018 World Wide Web Conference (Republic and Canton of Geneva, Switzerland, 2018), WWW \u201918, International World Wide Web Conferences Steering Committee, pp. 1155\u20131164."},{"key":"e_1_3_2_1_18_1","volume-title":"AMW","author":"Kim Y. W.","year":"2019","unstructured":"Kim , Y. W. , Consens , M. P. , and Hartig , O . An empirical analysis of GraphQL API schemas in open code repositories and package registries . In AMW ( 2019 ). Kim, Y. W., Consens, M. P., and Hartig, O. An empirical analysis of GraphQL API schemas in open code repositories and package registries. In AMW (2019)."},{"key":"e_1_3_2_1_19_1","volume-title":"Mathematical components. https:\/\/mathcomp.github.io\/mcb\/","author":"Mahboubi A.","year":"2018","unstructured":"Mahboubi , A. , and Tassi , E . Mathematical components. https:\/\/mathcomp.github.io\/mcb\/ , 2018 . Mahboubi, A., and Tassi, E. Mathematical components. https:\/\/mathcomp.github.io\/mcb\/ , 2018."},{"key":"e_1_3_2_1_20_1","volume-title":"RESTful Web APIs: Services for a Changing World . \" O\u2019Reilly Media","author":"Richardson L.","year":"2013","unstructured":"Richardson , L. , Amundsen , M. , Amundsen , M. , and Ruby , S . RESTful Web APIs: Services for a Changing World . \" O\u2019Reilly Media , Inc .\", 2013 . Richardson, L., Amundsen, M., Amundsen, M., and Ruby, S. RESTful Web APIs: Services for a Changing World . \" O\u2019Reilly Media, Inc.\", 2013."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the ISWC 2018 Posters & Demonstrations, Industry and Blue Sky Ideas Tracks co-located with 17th International Semantic Web Conference (ISWC 2018","author":"Taelman R.","year":"2018","unstructured":"Taelman , R. , Sande , M. V. , and Verborgh , R . GraphQL-LD: Linked data querying with GraphQL . In Proceedings of the ISWC 2018 Posters & Demonstrations, Industry and Blue Sky Ideas Tracks co-located with 17th International Semantic Web Conference (ISWC 2018 ), Monterey, USA, October 8th - to - 12th , 2018 . (2018). Taelman, R., Sande, M. V., and Verborgh, R. GraphQL-LD: Linked data querying with GraphQL. In Proceedings of the ISWC 2018 Posters & Demonstrations, Industry and Blue Sky Ideas Tracks co-located with 17th International Semantic Web Conference (ISWC 2018), Monterey, USA, October 8th - to - 12th, 2018. (2018)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3144826.3145437"},{"key":"e_1_3_2_1_24_1","first-page":"295","volume-title":"International Conference on Service-Oriented Computing","author":"Vogel M.","year":"2017","unstructured":"Vogel , M. , Weber , S. , and Zirpins , C . Experiences on migrating RESTful web services to GraphQL . In International Conference on Service-Oriented Computing ( 2017 ), Springer , pp. 283\u2013 295 . Vogel, M., Weber, S., and Zirpins, C. Experiences on migrating RESTful web services to GraphQL. In International Conference on Service-Oriented Computing (2017), Springer, pp. 283\u2013295."},{"key":"e_1_3_2_1_25_1","volume-title":"An empirical study of GraphQL schemas","author":"Wittern E.","year":"2019","unstructured":"Wittern , E. , Cha , A. , Davis , J. C. , Baudart , G. , and Mandel , L . An empirical study of GraphQL schemas , 2019 . Wittern, E., Cha, A., Davis, J. C., Baudart, G., and Mandel, L. An empirical study of GraphQL schemas, 2019."},{"key":"e_1_3_2_1_26_1","first-page":"83","volume-title":"Web Engineering (Cham","author":"Wittern E.","year":"2018","unstructured":"Wittern , E. , Cha , A. , and Laredo , J. A . Generating GraphQL-wrappers for REST(-like) APIs . In Web Engineering (Cham , 2018 ), T. Mikkonen, R. Klamma, and J. Hern\u00e1ndez, Eds., Springer International Publishing , pp. 65\u2013 83 . Wittern, E., Cha, A., and Laredo, J. A. Generating GraphQL-wrappers for REST(-like) APIs. In Web Engineering (Cham, 2018), T. Mikkonen, R. Klamma, and J. Hern\u00e1ndez, Eds., Springer International Publishing, pp. 65\u201383."},{"key":"e_1_3_2_1_27_1","volume-title":"GraphQL: Overlapping fields can be merged fast. https:\/\/tinyurl. com\/y3wqmnrw","author":"XING.","year":"2019","unstructured":"XING. GraphQL: Overlapping fields can be merged fast. https:\/\/tinyurl. com\/y3wqmnrw , 2019 . [Online; accessed 20-Sept-2019]. XING. GraphQL: Overlapping fields can be merged fast. https:\/\/tinyurl. com\/y3wqmnrw , 2019. [Online; accessed 20-Sept-2019]."}],"event":{"name":"POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"New Orleans LA USA","acronym":"POPL '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373822","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372885.3373822","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:09Z","timestamp":1750200069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373822"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,20]]},"references-count":26,"alternative-id":["10.1145\/3372885.3373822","10.1145\/3372885"],"URL":"https:\/\/doi.org\/10.1145\/3372885.3373822","relation":{},"subject":[],"published":{"date-parts":[[2020,1,20]]},"assertion":[{"value":"2020-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}