Statix - A Language for Static Semantics

Hendrik van Antwerpen


Date: Wed, February 21, 2018
Time: 12:00
Room: HG.2.66 (Faculty of CEG)


The static semantics of a programming language describes aspects such as program types, name resolution, or overload resolution. Static semantics can be described in terms of relations. For example, expressions are related to their types by a typing relation, and types are related to each other with a subtype relation. The meta-language NaBL2 allows the specification of static semantics by defining a relation over programs in terms of equality and name resolution constraints. However, expressing non-program-oriented relations such as type-based overloading, custom type relations such as structural subtyping, or name disambiguation was mostly impossible. In this talk we present Statix, a language to specify static semantics, that addresses these limitations. Statix is inspired by ideas from logic programming, and supports user-defined relations on top of builtin theories such as term equality and scope graph based name resolution. These relations are defined in terms of guarded simplification rules. We introduce the language using examples, showing cases such as type-based overloading, and structural record types with subtyping. We discuss some challenges related to the implementation of a sound solver for this language, and discuss directions for further work.

Previous: Wiebe van Geest |
Next: Victor Miraldo |