A Reconstruction of the Statix Constraint Language

Reuben Rowe

I will present some work-in-progress on recasting the Statix language more closely in the standard mold of a substructural, or resource, logic. The goal, as for Statix, is to obtain a framework for declaratively specifying static semantics of programming languages using the scope graph model, but one in which we might more easily obtain (complete) descision procedures for satisfiability, model checking/construction, etc. Key features of the approach include allowing “floating” edges in scope graphs, as well as taking only a basic reachability predicate as primitive and deriving more complex notions of query. I will describe how to specify Simply Typed Lambda Calculus using Scope Logic, and then extend this to the Hindley-Milner (ML) type system. I will highlight a general schema: specifications are split into a “spatial” part that describes only the local structure of an underlying scope graph, and a “pure” assertion over this graph that specifies constraints on the data it contains and reachability within it. The background for this work is the “Scopes As Types” paper, and the “Knowing When To Ask” manuscript.

---

Previous: group discussion | Getting Things Done
Next: Jonas Kastberg Hinrichsen | Machine-Checked Semantic Session Typing