A Constraint-based Approach to Name Binding and Type Checking using Scope Graphs

Recently scope graphs were introduced as a formalism to specify the name binding structure of a program and do name resolution independent of the abstract syntax tree of a program. In this thesis we show how to use a constraint language based on scope graphs to do static analysis of programs. We do this by extracting constraints from a program, that specify name binding and typing. We treat binding and typing as separate building blocks, but our approach allows language constructs – such as access of record fields – where name and type resolution are mutually dependent. By using scope graphs for name resolution, our approach supports a wide range of name binding patterns that are not easily supported in existing constraint-based approaches. We present a formal semantics for our constraint language, as well as a solver algorithm, for which we discuss soundness, termination and completeness of the solver. We evaluate our approach by expressing the static semantics of PCF and Featherweight Java with our constraints, and we implemented the solver algorithm, as well as static analysis for both languages, in the Spoofax language workbench.

Subject

Programming Languages
Static Program Analysis
Type Checking
Name Resolution
Constraint Solving

To reference this document use:

http://resolver.tudelft.nl/uuid:7a555c92-ee75-4e64-b58b-d8f09662f412

Part of collection

Student theses

Document type

master thesis

Rights

Files

PDF

thesis-final.pdf

610.79 KB

Close viewer