related.tex

%!TEX root = ./main.tex
\section{Related Work}\label{sec:related}

% \paragraph{\gql.} 
To the best of our knowledge, the only formalization efforts around \gql are \HP~\cite{gqlph} and~\cite{olafschema}, which we have already discussed. The rest of the \gql literature focuses on practical issues such as creating \gql services and migrating REST-based web services \gql~\cite{improvingoeeu, ehriapi, gqlexperiences}, automatic migration~\cite{migratingapi}, and testing techniques~\cite{gqldeviation}. A couple of empirical studies analyze the structure of \gql schemas in commercial and open-source projects~\cite{empiricalgql, empiricalapi}, shedding interesting insights on \gql in practice.
% Although these provide , they do not provide guarantees \wrt the specification's correctness. 
% As far as we are aware, the only works on formalizing \gql are the present work and~\cite{gqlph}.
% Most of the academic research on \gql 
% Others focus on testing techniques for implemented \gql services or tools for 

Despite being used mostly for web services, there are efforts to extend notions used in \gql to other areas of database specification and querying. Hartig and Hidders~\cite{olafschema} use the \gql schema definition DSL to define the structure of property graphs, which can be linked to similar efforts to define the structure of graph databases~\cite{schemaval}. Taelman \etal study the transformation of \gql queries to \sparql~\cite{gqlsparql}; however we are not aware of any mechanized formalization of \sparql.

% \paragraph{Mechanization of query languages.} 
The mechanized formalization of data management systems has received a lot of attention in the traditional relational data model~\cite{relationalcoq}, SQL and its semantics~\cite{sqlequiv, hottsql, vesqlengines, vesqlsemantics}, as well as related query languages and engines~\cite{certifdatalog, qcert}.
% \td{I had forgotten to include Q*Cert}. 
\coq is the proof assistant of choice for all these efforts. The tree-based nature of \gql queries and response differs significantly from the tuple-based semantics in traditional query languages, requiring different models and techniques.
% Although these efforts extensively cover these models and languages, we believe they are 
% not directly applicable to the \gql setting\td{One of the reasons is that queries and responses in \gql are both trees (the atomic response IS a tree), while }. 
% \td{Idk what to say tbh. I believe most of this work doesn't directly apply to our context, but it exists and cover several topics.}
% \td{Also, I am not an expert in databases and query languages, so I am not entirely sure how or what to compare}
% \td{I remember having a talk with Jorge where he mentioned that \gql is a lot simpler and that, although he thought they can be related to AQL, 
% they might not, because of this tree form of queries and responses -- which differs completely from the list of tuples in other query languages}
% \paragraph{Mechanization of graph data model.} 
Doczkal and Pous~\cite{graphtheory} develop a mechanization of graph theory in \coq, including simple graphs, digraphs, and their properties. Their work could possibly be extended to deal with property graphs, and used for \gcoql.
Bonifati \etal~\cite{graphviewmaint} build a Coq incremental graph view maintenance and evaluation engine; they experimentally assessed it on synthetic graphs generated from real-world schemas. The engine supports Regular Datalog queries and does not entirely fit the GraphQL setting; it could however serve as a base to extend \gcoql with mutation.
% Bonifati \etal~\cite{graphviewmaint} study graph view maintenance. Their definition of graphs is tailored to handle regular Datalog queries and does not entirely fit the \gql setting; it could however serve as a base to extend \gcoql with mutation.

% There is also work on 
% \td{They define a function that given a regexp returns a whole graph of the nodes that are connected via the regexp. Nodes are not typed, nor do they have properties I believe (not sure).}

% \paragraph{\gql miscellaneous.} 

% \et{is there any mechanized formalization of sparql?}\td{Haven't found one yet!}
% using \gql for deductive database in a Prolog setting~\cite{gqldeductive}. 
% \td{Not entirely sure what the last one is tbh, so probably	kill xd}


% \td{Mention the JSON formalization done by reutter?~\cite{json}}\et{what could we do with it? is there anything interesting to say? (eg. for responses?)}
% \td{Not sure. I looked at it when I was confused with HP's responses and thought I could base it off of it, but their formalization is a bit different than what I was expecting.
% They mention that theirs is the first formalization, but idk}