A Reconstruction of the Statix Constraint Language

Reuben Rowe

Date: Wed, May 20, 2020
Time: 12:00
Room: Eelco's Zoom Room

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 |
Next: Jonas Kastberg Hinrichsen |