Type Checkers from Declarative Type System Specifications in Statix
Eelco Visser
Seminar talk at Seminaire Cambium at INRIA, Paris | PDF
February 20, 2020

In this talk I present the design of Statix, a new constraint-based language for the executable specification of type systems. Statix specifications consist of predicates that define the well-formedness of language constructs in terms of built-in and user-defined constraints. Statix has a declarative semantics that defines whether a model satisfies a constraint. The operational semantics of Statix is defined as a sound constraint solving algorithm that searches for a solution for a constraint. The aim of the design is that Statix users can ignore the execution order of constraint solving and think in terms of the declarative semantics.

A distinctive feature of Statix is its use of scope graphs, a language parametric framework for the representation and querying of the name binding facts in programs. Since types depend on name resolution and name resolution may depend on types, it is typically not possible to construct the entire scope graph of a program before type constraint resolution. In (algorithmic) type system specifications this leads to explicit ordering of the construction and querying of the type environment (class table, symbol table). Statix automatically stages the construction of the scope graph of a program such that queries are never executed when their answers may be affected by future scope graph extension. In the talk, I will explain the design of Statix by means of examples and discuss the distinction between its declarative and operational semantics.

The code in the slides can be found in the paris project on github.

The design of Statix is based on the following publications:

  • Scopes as types. Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser. PACMPL 2(OOPSLA) 2018 [doi]

  • A constraint language for static semantic analysis based on scope graphs. Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. PEPM 2016 [doi]

  • A Theory of Name Resolution. Pierre Néron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. ESOP 2015 [doi]

Speaker: Eelco Visser (TU Delft) 

Bio: Eelco Visser is Professor of Computer Science and chair of the Programming Languages Group at Delft University of Technology. His current research is on the foundation and implementation of declarative specification of programming languages. The results of the research are integrated in the Spoofax Language Workbench (http://metaborg.org). For more information see http://eelcovisser.org.