main.tex

\documentclass[sigplan,balance,screen]{acmart}
\usepackage[utf8]{inputenc}
\usepackage{subcaption}
\usepackage{listings}
\usepackage{multicol}
\usepackage[cache=false]{minted}
\usepackage{listings}
\usepackage[nounderscore]{syntax}
\usepackage{graphicx}
\usepackage{xspace}
\usepackage{stmaryrd}
\usepackage{newunicodechar}
\newunicodechar{ə}{\pmschwa}
\DeclareRobustCommand{\pmschwa}{\rotatebox[origin=c]{180}{e}}
\usepackage{wrapfig}

%\linepenalty=20
%\clubpenalty=150
% \widowpenalty=150
% \parpenalty=-120


% Minted options
\setminted{fontsize=\footnotesize}
\definecolor{coqbg}{rgb}{0.95,0.95,0.95}


% Colors
\definecolor{darkgray}{HTML}{404040}
\definecolor{rulegray}{HTML}{DADADA}
\definecolor{keywordblue}{HTML}{1F497C}
\definecolor{mygray}{gray}{0.6}
% Listings
\lstdefinestyle{code}{
  basicstyle=\scriptsize,
  %backgroundcolor=\color{rulegray},
   numbers=left,
  emph=[1]{BEGIN, END, INPUT},
  emphstyle=[1]{\color{black}},
  keywordstyle=\color{keywordblue},
  keywords={LET, IN,CASE,IF,ELSE,THEN, WITH},
  escapeinside={(*@}{@*)}
}
% Listings
%\lstdefinestyle{code}{
  %basicstyle=\scriptsize,
  %keywordstyle=\color{keywordblue},
  %keywords={import,qualified,as,do,where}
%}


\newcommand{\mynote}[3]
    {{\color{#3} \fbox{\bfseries\sffamily\scriptsize#1}
    {\small$\blacktriangleright$\textsf{\emph{#2}}$\blacktriangleleft$}}~}
 \newcommand{\et}[1]{\mynote{ET}{#1}{purple}}
 \newcommand{\fo}[1]{\mynote{FO}{#1}{brown}}
 \newcommand{\td}[1]{\mynote{TD}{#1}{blue}}

% \newcommand{\et}[1]{}
% \newcommand{\fo}[1]{}
% \newcommand{\td}[1]{}


\newcommand\mdoubleplus{\mathbin{+\mkern-5mu+}}

% naming
\newcommand{\plstyle}[1]{\mbox{\textsc{#1}}\xspace}
\newcommand{\sparql}{\plstyle{SPARQL}}
\newcommand{\gql}{\plstyle{GraphQL}}
\newcommand{\gcoql}{\plstyle{GraphCoQL}}
\newcommand{\spec}{\plstyle{Spec}}
\newcommand{\HP}{\plstyle{H\&P}}
\newcommand{\json}{\plstyle{JSON}}
\newcommand{\jscert}{\plstyle{JSCert}}
\newcommand{\coqr}{\plstyle{CoqR}}
\newcommand{\coq}{\plstyle{Coq}}
\newcommand{\ssreflect}{\plstyle{Ssreflect}}
\newcommand{\mathcomp}{\plstyle{Mathematical Components}}
\newcommand{\equations}{\plstyle{Equations}}
\newcommand{\Vals}{$\mathit{Value}$\xspace}
\newcommand{\goodbois}{\plstyle{Artists}}
\newcommand{\movies}{\texttt{Movie}\xspace}
\newcommand{\fiction}{\texttt{Fiction}\xspace}
\newcommand{\animation}{\texttt{Animation}\xspace}
\newcommand{\artwork}{\texttt{Artwork}\xspace}
\newcommand{\artist}{\texttt{Artist}\xspace}

% math naming 
\newcommand{\query}{\varphi}
\newcommand{\sset}{\overline{\sigma}}
\newcommand{\sel}{\sigma}
\newcommand{\schema}{\mathcal{S}\xspace}
\newcommand{\graph}{\mathcal{G}\xspace}

\newcommand{\response}{\rho}
\newcommand{\ssize}[1]{\lvert #1 \rvert}

\newcommand{\name}{\mathit{name}}

% semantics
\newcommand{\filter}[2]{\mathit{filter(#2, #1)}}

\newcommand{\eval}[2]{\llbracket #1 \rrbracket^{#2}_{\graph}}
\newcommand{\evalu}[1]{\eval{#1}{u}}
\newcommand{\evalfilteru}[2]{\eval{\mathit{filter (#2, #1)}}{u}}
\newcommand{\collect}[3]{collect(#1, #2, #3)}
\newcommand{\ftype}[2]{ftype (#1, #2)}

% simpl semantics
\newcommand{\seval}[2]{\llparenthesis #1 \rrparenthesis^{#2}_{\graph}}
\newcommand{\sevalu}[1]{\seval{#1}{u}}

\newcommand{\queries}{\overline{\varphi}}
\newcommand{\subqueries}[1]{\overline{#1}}
\newcommand{\fkey}{\texttt{f}}

%selections
\newcommand{\args}{\overline{\alpha}}
\newcommand{\fld}{\texttt{f[}\args\texttt{]}}
\newcommand{\afld}{\texttt{a:}\fld}

 \newcommand{\nfld}[1]{\fld\; \texttt{\{}#1\texttt{\}} }
\newcommand{\anfld}[1]{\afld\; \texttt{\{}#1\texttt{\}} }

\newcommand{\ifrag}[2]{\texttt{... on #1 \{}#2\texttt{\}}}
\newcommand{\resp}[1]{\fkey\texttt{:}#1}
\newcommand{\nval}{\texttt{null}}
\newcommand{\val}{\texttt{v}}

%normalize
%\newcommand{\normalize}[1]{\mathit{normalize (#1)}}
\newcommand{\norm}[2]{\mathcal{N}_{\mathit{#1}}(#2)}
\newcommand{\tnorm}[1]{\norm{ts}{#1}}

%misc
\newcommand{\ie}{i.e.\@\xspace}
\newcommand{\wrt}{w.r.t.\@\xspace}
\newcommand{\eg}{e.g.\@\xspace}
\newcommand{\cf}{cf. \@\xspace}
\newcommand{\viz}{viz.\@\xspace}
\newcommand{\etal}{et al.\@\xspace}
\newcommand{\vscalar}{check\_scalar}


%\setcopyright{ACMUNKNOWN}
\copyrightyear{2020} 
\acmYear{2020} 
\setcopyright{acmlicensed}
\acmConference[CPP '20]{Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs}{January 20--21, 2020}{New Orleans, LA, USA}
\acmBooktitle{Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '20), January 20--21, 2020, New Orleans, LA, USA}
\acmPrice{15.00}
\acmDOI{10.1145/3372885.3373822}
\acmISBN{978-1-4503-7097-4/20/01}



\begin{document}

\title{A Mechanized Formalization of \gql}

\renewcommand\footnotemark{}
\titlenote{This work is partially funded by ERC Starting Grant SECOMP (715753).}

\author{Tomás Díaz}
\affiliation{%
  \institution{IMFD Chile}
%  \city{Santiago}
%  \country{Chile}
}
\email{tdiaz@imfd.cl}

\author{Federico Olmedo}
\affiliation{%<
  \institution{Computer Science Department\\ University of Chile \&
    IMFD Chile}
%  \department{Computer Science Department (DCC)}
  % \institution{University of Chile \& IMFD Chile}
  % \department{Computer Science Department (DCC)}
%  \city{Santiago}
%  \country{Chile}
}
\email{folmedo@dcc.uchile.cl}

\author{Éric Tanter}
\affiliation{%
  \institution{Computer Science Department\\ 
  U. of Chile \&
    IMFD Chile \& Inria Paris}
  % \institution{University of Chile \& IMFD Chile}
  % \department{Computer Science Department (DCC)}
%  \city{Santiago}
%  \country{Chile}
}
\email{etanter@dcc.uchile.cl}

\begin{abstract}
\gql is a novel language for specifying and querying web APIs,
allowing clients to flexibly and efficiently retrieve data of
interest. The \gql language specification is unfortunately only
available in prose, making it hard to develop robust formal results
for this language. Recently, Hartig and Pérez proposed a formal
semantics for \gql in order to study the complexity of \gql
queries. The semantics is however not mechanized and leaves certain key aspects unverified. We present \gcoql, the first mechanized formalization of \gql, developed in the \coq proof assistant.  \gcoql covers the schema definition DSL, query definitions, validation of both schema and queries, as well as the semantics of queries over a graph data model.
We illustrate the application of \gcoql by formalizing the key query transformation and interpretation techniques of Hartig and Pérez, and proving them correct, after addressing some imprecisions and minor issues. 
We hope that \gcoql can serve as a solid formal baseline for both language design and verification efforts for \gql.
\end{abstract}

\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10002951.10003260.10003304</concept_id>
<concept_desc>Information systems~Web services</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10002951.10002952.10003197</concept_id>
<concept_desc>Information systems~Query languages</concept_desc>
<concept_significance>300</concept_significance>
</concept>
<concept>
<concept_id>10003752.10010124</concept_id>
<concept_desc>Theory of computation~Semantics and reasoning</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}

\ccsdesc[500]{Information systems~Web services}
\ccsdesc[300]{Information systems~Query languages}
\ccsdesc[500]{Theory of computation~Semantics and reasoning}

\keywords{\gql, mechanized metatheory, \coq.}

\maketitle


\input{introduction.tex}
\input{background.tex}
\input{formalization.tex}
\input{normalization.tex}
\input{discussion.tex}
% \input{limitations.tex}
% \input{validation.tex}
\input{related.tex}
\input{conclusions.tex}

% \clearpage
\bibliographystyle{acm}
\bibliography{biblio}
\end{document}