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.
Wed 5 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30 | Session 4: Scopes & TypesEelco Visser Commemorative Symposium at Theatre Hall Chair(s): Yannis Smaragdakis University of Athens | ||
16:00 10mTalk | Scope Graphs: The Story so Far Eelco Visser Commemorative Symposium DOI Pre-print File Attached | ||
16:10 10mTalk | Dependently Typed Languages in Statix Eelco Visser Commemorative Symposium Jonathan Brouwer TU Delft, Jesper Cockx Delft University of Technology, Aron Zwaan Delft University of Technology Link to publication DOI | ||
16:20 10mTalk | Stack graphs: Name Resolution at Scale Eelco Visser Commemorative Symposium DOI Pre-print | ||
16:30 10mTalk | Using Spoofax to Support Online Code Navigation Eelco Visser Commemorative Symposium Peter D. Mosses Delft University of Technology DOI File Attached | ||
16:40 10mTalk | Renamingless Capture-Avoiding Substitution for Definitional Interpreters Eelco Visser Commemorative Symposium Casper Bach Poulsen Delft University of Technology DOI Pre-print | ||
16:50 10mTalk | Reasoning About Paths in the Interface Graph Eelco Visser Commemorative Symposium Michael Greenberg Stevens Institute of Technology Link to publication DOI | ||
17:00 10mTalk | Type Theory as a Language Workbench Eelco Visser Commemorative Symposium Jan de Muijnck-Hughes University of Glasgow, Guillaume Allais University of St Andrews, Edwin Brady University of St Andrews, UK Pre-print | ||
17:10 10mTalk | A Simply Numbered Lambda Calculus Eelco Visser Commemorative Symposium Friedrich Steimann Fernuniversität in Hagen Link to publication DOI | ||
17:20 10mOther | Session closing Eelco Visser Commemorative Symposium |