Coq specification for abstract GraphQL

[mstn]

EDIT changed to epic, not so easy

First, I would like to verify properties of the abstract syntax in a formal way. In this way I can double check the pen-and-pencil results of the notes. Writing derivation trees in html and css is otherwise error prone.

Then, I would like to test the formal semantics on a test suite. In other words I would like to be sure that the abstract language I am defining is as close as possible to (one of) the actual implementation(s) of GraphQL. The easiest way is to extract an interpreter from a Coq spec and try it with existing test suites.