  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) -- 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. This paper is under consideration for acceptance
in TPLP.
