Programming Languages and Tools Lab

Cypher’s Mechanization

Formalization of Cypher, a graph query language, in Coq.

This project aims to formalize Cypher, a graph query language, in the Coq proof assistant. 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.

Participants

Anton Podkopaev