Dependently Typed Languages in Statix

Title

Dependently Typed Languages in Statix

 Author

Brouwer, Jonathan (Student TU Delft)
Cockx, J.G.H. (TU Delft Programming Languages)
Zwaan, A.S. (TU Delft Programming Languages) ORCID 0000-0002-1818-4245

 Contributor

Lammel, Ralf (editor)
Mosses, Peter D. (editor)
Steimann, Friedrich (editor)

Date

2023

 Abstract

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.


 Subject

Calculus of Constructions
Dependent Types
Scope Graphs
Spoofax
Statix

 To reference this document use:

http://resolver.tudelft.nl/uuid:cfe5ad16-3938-4ab5-b438-a8220a15f068

 DOI

https://doi.org/10.4230/OASIcs.EVCS.2023.6

 Publisher

Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

 ISBN

9783959772679

 Source

Eelco Visser Commemorative Symposium, EVCS 2023

 Event

2023 Eelco Visser Commemorative Symposium, EVCS 2023, 2023-04-05, Delft, Netherlands

 Series

OpenAccess Series in Informatics, 2190-6807, 109

 Part of collection

Institutional Repository

 Document type

conference paper

 Rights

© 2023 Jonathan Brouwer, J.G.H. Cockx, A.S. Zwaan
Files
PDF OASIcs_EVCS_2023_6.pdf 627.2 KB
Close viewer