type-dependent name resolution

In our ESOP 2015 paper on A Theory of Name Resolution we presented a semantic framework for specification of the name binding patterns in programming languages. We are working on extending this framework with type analysis in order to support declarative specification of type systems. In this technical report we discuss our first results in this direction. We use constraints to formalize type analysis and connect these constraints to the references and declarations in scope graphs to provide a typing context to the names in programs. The connection between names and types is especially interesting in cases where type analysis is needed to perform name resolution, i.e. type-dependent name resolution. This occurs in programming languages in constructs such as field and method access in object-oriented languages, or in with expressions (inspired by Pascal's with statement). Figure 6 from the paper illustrates how such binding patterns are expressed in our framework using a combination of scope graph and constraints. We have a prototype implementation for the framework performing constraint resolution, and we have a prototype of a new version of our name binding and type analysis DSLs NaBL/TS targeting this framework as back-end.

Hendrik van Antwerpen, Pierre Neron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. Language-Independent Type-Dependent Name Resolution. Technical Report TUD-SERG-2015-006, Delft University of Technology, Software Engineering Research Group, Delft, The Netherlands, July 2015. [researchr, PDF]

Abstract: We extend and combine two existing declarative formalisms, the scope graphs of Neron et al. and type constraint systems, to build a language-independent theory that can describe both name and type resolution for realistic languages with complex scope and typing rules. Unlike conventional static semantics presentations, our approach maintains a clear separation between scoping and typing concerns, while still being able to handle language constructs, such as class field access, for which name and type resolution are necessarily intertwined. We define a constraint scheme that can express both typing and name binding constraints, and give a formal notion of constraint satisfiability together with a sound algorithm for finding solutions in important special cases. We describe the details of constraint generation for a model language that illustrates many of the interesting resolution issues associated with modules, classes, and records. Our constraint generator and solver have been implemented in the Spoofax Language Workbench.

In response to popular demand I have created a Spoofax project for LBNF, the grammar formalism of the BNFC project. The project contains an SDF3 definition for LBNF obtained by manually converting the LBNF grammar in LBNF, and a transformation from LBNF to SDF3.

The transformation is fairly straightforward since LBNF and SDF3 productions are similar. In particular, LBNF productions declare a constructor symbol, which is also needed in SDF3. The main distinction is the way that lists are specified. For example, the following LBNF productions

    Rule . Def ::= Label "." Cat "::=" [Item] ;
    []  . [Item] ::= ;
    (:) . [Item] ::= Item [Item] ;

translate to this SDF3 production:

    Def.Rule = [[Label] . [Cat] ::= [{Item " "}*]]

The transformation is probably somewhat rudimentary and ignores advanced features of LBNF. Yet the converter should be fairly robust, since it skips anything that it doesn't recognize. I have only tested it on the LBNF.cf file itself. More testing is needed. I will be happy to do some more work on the transformation if popular demand so requires.

Using LBNF to SDF3

To use the converter:

  • Check out the GitHub repository (https://github.com/MetaBorgCube/metaborg-lbnf) and import the project into your Eclipse with Spoofax.
  • Build the project.
  • Open a .cf file
  • Hit the 'Transform to SDF3' transformation in the 'Generation' menu
Read more

I have started writing a book about declarative language definition with the Spoofax Language Workbench. The first chapter about Getting Spoofax is done. The chapter explains how to get started for Eclipse newbies. In particular, Spoofax is now shipped as a complete Eclipse installation including JRE and the appropriate patches to the 'eclipse.ini' file, so that it should be easy to get started. In the next chapters I will be discussing the definition of a language using Spoofax from a user perspective.

The project is on GitHub and there's a website with a link to latest version:


The book is a PDF in a format that is intended for reading on tablets (e.g. using the GoodReader app on iPad), i.e. big letters and no margins.

The source code of the book and of the accompanying Spoofax projects are all in the GitHub repository, so that it is easy to provide contributions, from typo fixes to entire chapters. Pull requests are welcome.

I'll update this post with news about new chapters.

Read more

After declarative syntax definition and declarative name binding, our next milestone on the road to a language designer's workbench is DynSem, a DSL for the specification of dynamic semantics. The DynSem prototype implementation is integrated as an experimental feature in the Spoofax Language Workbench (in the nightly build edition). In the coming months we will be further improving that integration and the documentation of DynSem. For now, there is this paper to be presented at the RTA 2015 conference:

DynSem: A DSL for Dynamic Semantics Specification by Vlad Vergu, Pierre Neron, and Eelco Visser. To appear in the proceedings of RTA 2015. Preprint PDF.

Abstract: The formal definition the semantics of a programming language and its implementation are typically separately defined, with the risk of divergence such that properties of the formal semantics are not properties of the implementation. In this paper, we present DynSem, a domain-specific language for the specification of the dynamic semantics of programming languages that aims at supporting both formal reasoning and efficient interpretation. DynSem supports the specification of the operational semantics of a language by means of statically typed conditional term reduction rules. DynSem supports concise specification of reduction rules by providing implicit build and match coercions based on reduction arrows and implicit term constructors. DynSem supports modular specification by adopting implicit propagation of semantic components from I-MSOS, which allows omitting propagation of components such as environments and stores from rules that do not affect those. DynSem supports the declaration of native operators for delegation of aspects of the semantics to an external definition or implementation. DynSem supports the definition of auxiliary meta-functions, which can be expressed using regular reduction rules and are subject to semantic component propagation. DynSem specifications are executable through automatic generation of a Java-based AST interpreter.

My slides for a talk on WebLab March 9, 2015 at the Research Seminar on Data Science, organized as part of the TU Delft events around Open Education Week 2015.

The recording of the talk is online as well.