Statix - Typechecking with Scope Graphs and Constraints

Hendrik van Antwerpen

In this talk I will present Statix, a meta-language for writing type checkers. Statix is a constraint language with built-in support for scope graphs. It builds on the concepts of the constraint language underlying NaBL2, but increases expressivity by generalizing the constraints and aspects of scope graph resolution. I will show examples to highlight interesting language features, and discuss our follow-up efforts.

---

Previous: Daco Harkes | Aim, Relevance, Methods, Results, and Evidence in IceDust Research
Next: Robbert Krebbers | Mtac2 - Typed Tactics for Backward Reasoning in Coq