{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T14:50:08Z","timestamp":1758120608592,"version":"3.37.3"},"reference-count":38,"publisher":"Cambridge University Press (CUP)","issue":"3-4","license":[{"start":{"date-parts":[[2018,8,10]],"date-time":"2018-08-10T00:00:00Z","timestamp":1533859200000},"content-version":"unspecified","delay-in-days":40,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2018,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular Datalog (RD) \u2013 a notable fragment of non-recursive Datalog that can express complex navigational queries, with transitive closure as native operator. We first design and encode the theory of RD and then mechanize a RD-specific evaluation algorithm capable of fine-grained, incremental graph view computation, which we prove sound with respect to the declarative RD semantics. By using the Coq extraction mechanism, we test an OCaml version of the verified engine on a set of preliminary benchmarks. Our development is particularly focused on leveraging existing verification and notational techniques to: a) define mechanized properties that can be easily understood by logicians and database researchers and b) attain formal verification with limited effort. Our work is the first step towards a unified, machine-verified, formal framework for dynamic graph query languages and their evaluation engines.<\/jats:p>","DOI":"10.1017\/s1471068418000224","type":"journal-article","created":{"date-parts":[[2018,8,10]],"date-time":"2018-08-10T09:44:17Z","timestamp":1533894257000},"page":"372-389","source":"Crossref","is-referenced-by-count":7,"title":["Certified Graph View Maintenance with Regular Datalog"],"prefix":"10.1017","volume":"18","author":[{"given":"ANGELA","family":"BONIFATI","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6664-0620","authenticated-orcid":false,"given":"STEFANIA","family":"DUMBRAVA","sequence":"additional","affiliation":[]},{"given":"EMILIO JES\u00daS GALLEGO","family":"ARIAS","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2018,8,10]]},"reference":[{"key":"S1471068418000224_ref34","unstructured":"Oracle PGX. http:\/\/www.oracle.com\/technetwork\/oracle-labs\/parallel-graph- analytix (visited: 2018-02)."},{"key":"S1471068418000224_ref21","unstructured":"FlockDB. https:\/\/github.com\/twitter-archive\/flockdb (visited: 2018-02)."},{"key":"S1471068418000224_ref22","unstructured":"G-Core. https:\/\/github.com\/ldbc\/ldbc_gcore_parser (visited: 2018-02)."},{"key":"S1471068418000224_ref25","unstructured":"GraphQL. http:\/\/graphql.org\/ (visited: 2018-02)."},{"key":"S1471068418000224_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"S1471068418000224_ref19","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1145\/2723372.2742786","volume-title":"Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data","author":"Erling","year":"2015"},{"key":"S1471068418000224_ref9","first-page":"189","volume-title":"Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410","author":"Benzaken","year":"2014"},{"key":"S1471068418000224_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_12"},{"key":"S1471068418000224_ref7","doi-asserted-by":"crossref","first-page":"1555","DOI":"10.1145\/3035918.3035961","volume-title":"Proceedings of the 2017 ACM International Conference on Management of Data","author":"Auerbach","year":"2017"},{"key":"S1471068418000224_ref37","unstructured":"SPARQL. https:\/\/www.w3.org\/TR\/sparql11-query\/ (visited: 2018-02)."},{"key":"S1471068418000224_ref12","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1145\/2594291.2594304","volume-title":"Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Cai","year":"2014"},{"key":"S1471068418000224_ref2","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-319-11964-9_13","volume-title":"The Semantic Web (ISWC 2014)","author":"Alu\u00e7","year":"2014"},{"key":"S1471068418000224_ref4","unstructured":"Anand A. , Appel A. W. , Morrisett G. , Paraskevopoulou Z. , Pollack R. , B\u00e9langer O. S. , Sozeau M. , and Weaver M. 2017. Certicoq: A verified compiler for Coq. In CoqPL 2017: The 3rd International Workshop on Coq for Programming Languages."},{"key":"S1471068418000224_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00079-8"},{"key":"S1471068418000224_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-016-9676-2"},{"key":"S1471068418000224_ref20","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1145\/3035918.3035944","volume-title":"Proceedings of the 2017 ACM International Conference on Management of Data","author":"Fan","year":"2017"},{"key":"S1471068418000224_ref16","first-page":"293","volume-title":"Logic and Data Bases","author":"Clark","year":"1977"},{"key":"S1471068418000224_ref8","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2016.2633993"},{"key":"S1471068418000224_ref33","unstructured":"Neo4j. https:\/\/neo4j.com\/ (visited: 2018-02)."},{"key":"S1471068418000224_ref11","first-page":"57","article-title":"Incremental view maintenance for deductive graph databases using generalized discrimination networks","volume":"231","author":"Beyhl","year":"2016","journal-title":"GaM@ETAPS"},{"key":"S1471068418000224_ref38","unstructured":"The Coq Development Team. 2018. The Coq proof assistant, version 8.7.2."},{"key":"S1471068418000224_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"S1471068418000224_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3104031"},{"key":"S1471068418000224_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/170036.170066"},{"key":"S1471068418000224_ref3","doi-asserted-by":"crossref","unstructured":"Alviano M. , Calimeri F. , Dodaro C. , Fusc\u00e0 D. , Leone N. , Perri S. , Ricca F. , Veltri P. , and Zangari J. 2017. The ASP system DLV2. In Logic Programming and Nonmonotonic Reasoning LPNMR 2017. 215\u2013221.","DOI":"10.1007\/978-3-319-61660-5_19"},{"key":"S1471068418000224_ref17","unstructured":"Cohen C. and Th\u00e9ry L. 2017. Full script of Tarjan SCC Coq\/SSreflect proof. Tech. rep., INRIA. https:\/\/github.com\/CohenCyril\/tarjan (visited: 2018-02)."},{"key":"S1471068418000224_ref27","unstructured":"Gremlin. http:\/\/tinkerpop.apache.org\/ (visited: 2018-02)."},{"key":"S1471068418000224_ref23","unstructured":"Giraph. http:\/\/giraph.apache.org\/ (visited: 2018-02)."},{"key":"S1471068418000224_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"volume-title":"Foundations of Databases: The Logical Level","year":"1995","author":"Abiteboul","key":"S1471068418000224_ref1"},{"key":"S1471068418000224_ref32","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1145\/3167089","volume-title":"Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs","author":"Mullen","year":"2018"},{"key":"S1471068418000224_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/38714.38750"},{"key":"S1471068418000224_ref6","doi-asserted-by":"crossref","unstructured":"Aref M. , ten Cate, B. , Green T. J. , Kimelfeld B. , Olteanu D. , Pasalic E. , Veldhuizen T. L. , and Washburn G. 2015. Design and implementation of the LogicBlox system. In Proceedings of ACM SIGMOD. 1371\u20131382.","DOI":"10.1145\/2723372.2742796"},{"key":"S1471068418000224_ref14","doi-asserted-by":"publisher","DOI":"10.1109\/69.43410"},{"key":"S1471068418000224_ref13","unstructured":"Cayley. https:\/\/github.com\/cayleygraph\/cayley (visited: 2018-02)."},{"key":"S1471068418000224_ref18","unstructured":"Cypher. https:\/\/www.opencypher.org\/ (visited: 2018-02)."},{"key":"S1471068418000224_ref26","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195085914.001.0001","volume-title":"Limits to Parallel Computation: P-completeness Theory","author":"Greenlaw","year":"1995"},{"key":"S1471068418000224_ref15","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1145\/3062341.3062348","volume-title":"Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Chu","year":"2017"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068418000224","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:58:16Z","timestamp":1661734696000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068418000224\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":38,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2018,7]]}},"alternative-id":["S1471068418000224"],"URL":"https:\/\/doi.org\/10.1017\/s1471068418000224","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2018,7]]}}}