Last Thursday, Hendrik van Antwerpen defended his master’s thesis A Constraint-based Approach to Name Binding and Type Checking using Scope Graphs. On January 19, 2016 he will present the related paper at PEPM 2016.

Abstract: 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.

SERG is looking to strengthen its Programming Languages research program under the leadership of Prof. Dr. Eelco Visser. We aim at a broad program connecting logic, programming languages, and software engineering in order to improve the correctness, reliability, and security of software by using high-level, domain-specific formal specifications supported by tools such as certified compilers, model checkers, SMT solvers, and/or proof assistants. To that end, we are looking for an assistant professor to complement our current research strengths in language engineering and domain-specific languages with expertise in one or more of the following topics

  • Software verification
  • Language-based security
  • Semantics engineering
  • Software synthesis
  • Program analysis
  • Type systems
  • Execution engines
  • Performance engineering

We welcome researchers with an interest in programming language research inspired by applications to data science (Delft Data Science), cyber security (3TU Cyber Security master specialization), online learning, and/or quantum computing.

Read more

On July 13 I gave a hands-on tutorial on language definition with Spoofax at the Summer School on DSL Design and Implementation at EPFL in Lausanne. Here is the original abstract and the recordings of the execution of the tutorial.

Language workbenches are tools aiming to reduce the gap between the design and implementation of (external domain-specific) programming languages. Given high-level descriptions of the syntax and semantics of a language, a workbench generates an implementation of an IDE and/or execution engine. There are many different approaches to realising these goals. In this session I will demonstrate and discuss the state of declarative language definition in the Spoofax Language Workbench.

In the first part of the session I give a hands-on tutorial of the development of language front-ends with Spoofax. We will explore syntax definition in SDF3, name binding and scope rules in NaBL, and type constraints in TS. Participants are expected to bring a (decently equipped) laptop with Eclipse/Spoofax and the exercise projects pre-installed according to the instructions provided at

In the second part I will present recent research in expanding declarative language definition. (1) In our ESOP15 paper we develop a theory of name resolution to provide a generalisation and post-hoc semantics of the concepts of the NaBL name binding language. I will present the scope graph model, its resolution calculus, and the application of scope graphs to model name binding patterns in existing languages. (2) Language workbenches typically employ code generation to give semantics to languages. This often leads to questions about the exact source-level semantics of the language. We are working on DynSem, a DSL for the specification of dynamic semantics aimed at rapid prototyping, generation of interpreters, and (eventually) verification of soundness properties. DynSem is based on the work of implicitly modular operational semantics of Peter Mosses. I will discuss the current state of the design of the language.

Unfortunately, the sound is missing in the second half of the second video.

If you missed this tutorial, there will be a new (updated) edition at POPL 2016 in St Petersburg, Florida on Monday, January 18, 2016.

The program of a large conference such as SPLASH can be rather overwhelming. It is easy to get lost in the large number of talks. And even when you go through the program before the conference, you may not remember your selection while there. So, to help with that, we added support for personal schedules to the application, which should be useful to you if you’ll be attending any of the conferences hosted on researchr. We think the feature is pretty easy to use; click the star icon of any talks you’d like to attend and select ‘Your Program’ to see your selection. I have created a short video to demonstrate the new feature.


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.