Dependently Typed Languages in Statix
Master Project of Jonathan Brouwer

Abstract

Static type systems can greatly enhance the quality of programs, but implementing a type checker for them is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make this task easier by automatically deriving a type checker from a declarative specification of the type system. However, so far Statix has not been used to implement a type system with dependent types, an expressive class of type systems which require evaluation of terms during type checking.

In this thesis, we present a specification of a simple dependently typed language in Statix, and discuss how to extend it with several common features such as inductive data types, universes, and inference of implicit arguments. While we encountered some challenges in the implementation, our conclusion is that Statix is already usable as a tool for implementing dependent types.

Relevant Thesis

• Brouwer, Jonathan. Dependently Typed Languages in Statix. TU Delft Repository, 2023.

Related Publication

• Brouwer, J., Cockx, J., & Zwaan, A. (2023). Dependently Typed Languages in Statix. In R. Lammel, P. D. Mosses, & F. Steimann (Eds.), Eelco Visser Commemorative Symposium, EVCS 2023 [6] (OpenAccess Series in Informatics; Vol. 109). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.