Embedding Statix in Agda

Embedding Statix in Agda
Master Project of Alex Harsani

Problem statement

Statix is a domain-specific language for implementing type systems and other forms of static program analyses, and is a part of the Spoofax language workbench. By allowing the language designer to give a high-level declarative specification of the static analysis in question, the risk of accidental bugs and other mistakes in its implementation is greatly reduced. However, there is still the risk that there is a logical error in the specification of the analysis itself, which could lead to unsoundness or unpredictable behaviour. The state-of-the-art to prevent these kind of errors is to use a proof assistant such as Coq, Agda, or Lean to formally prove the correctness of the analysis.

Project description

The goal of this project is to build a bridge that can translate Statix specifications into the Agda proof assistant, in order to enable users of Spoofax to reason formally about their language specifications. An important prerequisite for this translation is to provide an embedding of (part of) the Statix language in Agda. In particular, scope graphs are a core building block of Statix and hence need to be defined in Agda. Because of the large scope of this project, it is possible that this task will occupy the majority of the thesis. If time allows, the next step would be to start work on an automated translation from Statix to Agda, and use this in one or more case studies.