Write a Blog >>
Tue 21 Jan 2020 10:51 - 11:13 at Maurepas - Mechanized metatheory Chair(s): Benjamin C. Pierce

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: (GMT-06:00) Saskatchewan, Central America change

CPP-2020-papers
10:30 - 11:35: CPP 2020 - Mechanized metatheory at Maurepas
Chair(s): Benjamin C. PierceUniversity of Pennsylvania
CPP-2020-papers10:30 - 10:51
Talk
Yannick ForsterSaarland University, Kathrin StarkSaarland University, Germany
DOI Pre-print Media Attached
CPP-2020-papers10:51 - 11:13
Talk
Tomás DíazIMFD Chile, Federico OlmedoUniversity of Chile & IMFD Chile, Éric TanterUniversity of Chile
DOI Pre-print Media Attached File Attached
CPP-2020-papers11:13 - 11:35
Talk
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