Programmiersprachen und Tools Lab

Cypher’s Mechanization

Formalisierung von Cypher, einer Graphenabfragesprache, in Coq.

Dieses Projekt zielt darauf ab, Cypher, eine Graphenabfragesprache, im Coq Beweisassistenten zu formalisieren. Der Zweck der Formalisierung ist es, eine solide Grundlage für die weitere Entwicklung der Sprache zu schaffen und einen Rahmen für die Verifizierung von Optimierungen von Abfragen zu bieten.

Teilnehmende

Anton Podkopaev