Print Email Facebook Twitter Dependently Typed Languages in Statix Title Dependently Typed Languages in Statix Author Brouwer, Jonathan (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor van Deursen, A. (mentor) Cockx, J.G.H. (graduation committee) Zwaan, A.S. (mentor) Degree granting institution Delft University of Technology Programme Computer Science Date 2023-04-26 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. Subject SpoofaxStatixDependent TypesScope GraphsCalculus of Constructions To reference this document use: http://resolver.tudelft.nl/uuid:7bf3c0f5-71fb-4e08-bcdb-1c873c7e1e63 Bibliographical note Source code - https://github.com/JonathanBrouwer/master-thesis Part of collection Student theses Document type master thesis Rights © 2023 Jonathan Brouwer Files PDF document.pdf 341.46 KB Close viewer /islandora/object/uuid:7bf3c0f5-71fb-4e08-bcdb-1c873c7e1e63/datastream/OBJ/view