EVCS
Wed 5 Apr 2023 Delft, Netherlands
Wed 5 Apr 2023 16:10 - 16:20 at Theatre Hall - Session 4: Scopes & Types Chair(s): Yannis Smaragdakis

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 Apr

Displayed 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
10m
Talk
Scope Graphs: The Story so Far
Eelco Visser Commemorative Symposium
Aron Zwaan Delft University of Technology, Hendrik van Antwerpen GitHub
DOI Pre-print File Attached
16:10
10m
Talk
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
10m
Talk
Stack graphs: Name Resolution at Scale
Eelco Visser Commemorative Symposium
DOI Pre-print
16:30
10m
Talk
Using Spoofax to Support Online Code Navigation
Eelco Visser Commemorative Symposium
Peter D. Mosses Delft University of Technology
DOI File Attached
16:40
10m
Talk
Renamingless Capture-Avoiding Substitution for Definitional Interpreters
Eelco Visser Commemorative Symposium
Casper Bach Poulsen Delft University of Technology
DOI Pre-print
16:50
10m
Talk
Reasoning About Paths in the Interface Graph
Eelco Visser Commemorative Symposium
Michael Greenberg Stevens Institute of Technology
Link to publication DOI
17:00
10m
Talk
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
10m
Talk
A Simply Numbered Lambda Calculus
Eelco Visser Commemorative Symposium
Friedrich Steimann Fernuniversität in Hagen
Link to publication DOI
17:20
10m
Other
Session closing
Eelco Visser Commemorative Symposium