A Mechanized Formalization of GraphQL
GraphQL is a novel language for specifying and querying web APIs, allowing clients to flexibility and efficiently retrieve data of interest. The GraphQL 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 GraphQL in order to study the complexity of GraphQL queries. This semantics is however not mechanized and leaves certain key aspects unverified. We present GraphCoQL, the first mechanized formalization of GraphQL, developed in the Coq proof assistant. GraphCoQL 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 GraphCoQL 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 GraphCoQL can serve as a solid formal baseline for both language design and verification efforts for GraphQL.
Slides (Slides - GraphCoQL.pdf) | 17.4MiB |
Tue 21 Jan Times are displayed in time zone: Saskatchewan, Central America change
10:30 - 11:35: Mechanized metatheoryCPP at Maurepas Chair(s): Benjamin C. PierceUniversity of Pennsylvania | |||
10:30 - 10:51 Talk | Coq à la Carte - A Practical Approach to Modular Syntax with Binders CPP DOI Pre-print Media Attached | ||
10:51 - 11:13 Talk | A Mechanized Formalization of GraphQL CPP Tomás DíazIMFD Chile, Federico OlmedoUniversity of Chile & IMFD Chile, Éric TanterUniversity of Chile DOI Pre-print Media Attached File Attached | ||
11:13 - 11:35 Talk | ConCert: A Smart Contract Certification Framework in Coq CPP Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University DOI Pre-print Media Attached File Attached |