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.

Update December 29, 2015: Here is a set of slides about DynSem developed for a lecture in our compiler construction course on November 24, 2015.

Dynamic Semantics Specification and Interpreter Generation from Eelco Visser

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.


In 2012 we introduced the NaBL name binding language, which supports high-level declarative specification of name binding and scope rules of (domain-specific) programming languages. In 2013 we introduced an incremental execution engine for NaBL, which recomputes only the resolution of those names that have been affected by a change. While this provides a powerful tool for language designers, we had a hard time explaining exactly how it worked. We kept getting the question ‘but what is the semantics of NaBL?’ and we didn’t have a good answer. Our attempts at formulating a high-level concise formalization of the semantics underlying the implementation proved that this was a non-trivial problem. In 2014 we finally managed to formulate a language-independent theory of name resolution in the form of a calculus that defines name resolution in a `scope graph’. The paper has been accepted for publication in the ESOP 2015 proceedings and is the ESOP nominee for the ETAPS 2015 best paper award:

A Theory of Name Resolution. Pierre Neron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. In Jan Vitek (editor), Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. 2015

We have published an extended version of the paper as a technical report: A theory of name resolution with extended coverage and proofs (PDF)

Abstract: We describe a language-independent theory for name binding and resolution, suitable for programming languages with complex scoping rules including both lexical scoping and modules. We formulate name resolution as a two stage problem. First a language-independent scope graph is constructed using language-specific rules from an abstract syntax tree. Then references in the scope graph are resolved to corresponding declarations using a language-independent resolution process. We introduce a resolution calculus as a concise, declarative, and language-independent specification of name resolution. We develop a resolution algorithm that is sound and complete with respect to the calculus. Based on the resolution calculus we develop language-independent definitions of alpha-equivalence and rename refactoring. We illustrate the approach using a small example language with modules. In addition, we show how our approach provides a model for a range of name binding patterns in existing languages.

Update April 15, 2015: The paper won the EAPLS 2015 Best Paper Award. ETAPS Daily

Last month I presented our paper about our vision of a language designer’s workbench at Onward! 2014 in Portland. Here are the slides of that presentation:

A Language Designer’s Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs. Eelco Visser, Guido Wachsmuth, Andrew P. Tolmach, Pierre Neron, Vlad A. Vergu, Augusto Passalaqua, Gabriël Konat. OOPSLA 2014: 95-111

Abstract: The realization of a language design requires multiple artifacts that redundantly encode the same information. This entails significant effort for language implementors, and often results in late detection of errors in language definitions. In this paper we present a proof-of-concept language designer’s workbench that supports generation of IDEs, interpreters, and verification infrastructure from a single source. This constitutes a first milestone on the way to a system that fully automates language implementation and verification.

We have an opening for a PhD student to work on automatic grading and tutoring in online courses. In particular, we are interested in automatic feedback and assessment techniques that we can apply in programming education. The results of the research will be applied and evaluated in several courses at TU Delft and other universities.

We are looking for a candidate with a Master’s degree (or equivalent) in computer science or a related discipline, a passion for online education, and a broad interest including systems programming, compilers, language engineering, programming environments, web programming, machine learning, interaction design, education research, and teaching.

For more information about the position see