Dependently Typed Languages in Statix

Master thesis (2023)

Authors

J.T. Brouwer Electrical Engineering, Mathematics and Computer Science

Contributors

A. van Deursen Software Technology (mentor)
J.G.H. Cockx Programming Languages - EEMCS (graduation committee member)
A.S. Zwaan Programming Languages - EEMCS (mentor)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2023 Jonathan Brouwer
More Info
expand_more

Published Date

26-04-2023

Language

English

Reuse Rights

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.

Files

Document.pdf
(pdf | 0.333 Mb)
Unknown license