A Constraint Language for Static Semantic Analysis based on Scope Graphs

In July, we reported on our ongoing work to formalize the connection between name binding described with scope graphs and types, and in particular type-dependent name resolution in which name and type analysis are interdependent (and, as a result, cannot be staged). In a new technical report we present a generalization of that framework with as interface a constraint language that can serve as intermediate language for name and type analysis.

Hendrik van Antwerpen, Pierre Néron, Andrew Tolmach, Eelco Visser, and Guido Wachsmuth. A Constraint Language for Static Semantic Analysis based on Scope Graphs with Proofs. Technical Report TUD-SERG-2015-012, Delft University of Technology.

Abstract: In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs—such as record field access—for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records.

Update 20 October, 2015: The paper has been accepted at PEPM 2016

Update December 2015: New version of technical report reflecting the final revision for the conference.