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: Saskatchewan, Central America change

10:30 - 11:35: Mechanized metatheoryCPP at Maurepas
Chair(s): Benjamin C. PierceUniversity of Pennsylvania
10:30 - 10:51
Talk
CPP
Yannick ForsterSaarland University, Kathrin StarkPrinceton University, USA
DOI Pre-print Media Attached
10:51 - 11:13
Talk
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
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