Dependently Typed Languages in Statix

Jonathan Brouwer*, Jesper Cockx, Aron Zwaan

*Corresponding author for this work

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

25 Downloads (Pure)


Static type systems can greatly enhance the quality of programs, but implementing a type checker that is both expressive and user-friendly 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 a type system. However, so far Statix has not been used to implement dependent types, which is a class of type systems which require evaluation of terms during type checking. In this paper, we present an implementation 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.

Original languageEnglish
Title of host publicationEelco Visser Commemorative Symposium, EVCS 2023
EditorsRalf Lammel, Peter D. Mosses, Friedrich Steimann
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages8
ISBN (Electronic)9783959772679
Publication statusPublished - 2023
Event2023 Eelco Visser Commemorative Symposium, EVCS 2023 - Delft, Netherlands
Duration: 5 Apr 20235 Apr 2023

Publication series

NameOpenAccess Series in Informatics
ISSN (Print)2190-6807


Conference2023 Eelco Visser Commemorative Symposium, EVCS 2023


  • Calculus of Constructions
  • Dependent Types
  • Scope Graphs
  • Spoofax
  • Statix

Cite this