GraphCoQL: A mechanized formalization of GraphQL in Coq
summary
Mechanized formalization of GraphQL in Coq that defines a graph data model, implements a normalization algorithm and proves it correct and semantics-preserving for queries in normal form. Identifies flaws in the previous informal formalization: a broken normal form definition and incomplete equivalence rules. Provides a compositional simplified semantics for normalized queries and mechanizes example queries from the specification and the JavaScript reference, executing them in Coq successfully. Plans extraction to OCaml/Haskell for a certified reference implementation.
AI-written summary · about
chapters (7)
- 0:00Start
- 3:42Schema
- 4:27Enumeration Types
- 5:43Graph Data Model
- 6:53Root Node
- 7:35The Meaning of a Query in Graph
- 11:49Normalization Algorithm
related talks
29mA New Era for Graph Queries: ISO/IEC 39075 GQL
58mCoalgebra for the working programming languages researcher
31mA Coq Library of Undecidable Problems
27mAn Equations Tutorial
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
42mMetaCoq as a tool to prevent future unsoundness in Coq
19mInterpreting OCaml GADTs into Coq
29mMechanized monadic equational reasoning for ML references