Embedding Statix in Agda
A. Haršáni (TU Delft - Electrical Engineering, Mathematics and Computer Science)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Static type-checking allows us to detect ill-typed programs even before running them. However, the higher complexity of type systems may cause type-checker implementation to differ from their specifications. This causes bugs and makes it hard to reason about the type of systems. To close this gap between implementation and specification, a meta-language Statix was introduced. Using Statix, we can write a specification using constraints over scope graphs and terms. Successfully solving these constraints means that the program is well-typed. However, while Statix ensures that the implementation and specification correspond to each other, it does not offer a way for its users to formally reason about the type systems' specifications. To this end, we introduce a library called statix-in-agda. This library, written using the proof assistant Agda, includes the formalisation of scope graphs and embedding of Statix's constraints. We show how we can use our library to specify the type system of STLC-like language, prove that programs in this language are well-typed, and give type-preservation proof for a type system of a simple toy language with numbers and addition.