This project aims to formalize Cypher, a graph query language, in the Coq proof assistant. The formalization follows O.H. Morra’s paper “A Semantics of GQL. A New Query Language for Property Graph formalized”.
The purpose of the formalization is to make a rigid foundation for further evolution of the language as well as to provide a framework for verifying optimizations of queries.
The current release of the model can be downloaded from GitHub.
The coqdoc model’s presentations can be browsed online
Related article listed below (in progress) Формализация и верификация Cypher на Coq