The dutch national science foundation NWO has awarded the VICI proposal ‘The Language Designer’s Workbench’ to investigate the building blocks of the next generation of language workbenches. The essence of the plan is to provide much better support to language designers by means of deep analyses of language definitions.

Summary

Software systems are the engines of modern information society. Our ability to cope with the increasing complexity of software systems is limited by the programming languages we use to build them. Bridging the gap between domain concepts and the implementation of these concepts in a programming language is one of the core challenges of software engineering. Modern programming languages have considerably reduced this gap, but still require low-level programmatic encodings of domain concepts. Domain-specific software languages (DSLs) address this problem through linguistic abstraction by providing notation, analysis, verification, and optimization that are specialized to an application domain. Language workbenches assist language designers with the implementation of languages. However, DSL implementations rarely formally guarantee semantic correctness properties such as type soundness and behaviour preservation of transformations, since current language workbenches provide no support for such verification, which leads to intricate errors in language designs that are discovered late.

In this project, we will work towards new methods and techniques for automating verification of language definitions. The key innovations are: (1) High-level formalisms for the declarative specification of software languages that are declarative, multi-purpose, and generative as well as reductive; (2) Efficient and scalable language parametric algorithms for name resolution, type checking, and program execution; (3) Language parametric test generators that attempt to generate counter examples to type soundness and semantics preservation based on language definitions; (4) Language parametric proof engineering techniques to support automated verification of type soundness and semantics preservation.

The techniques will be integrated in the innovative Spoofax Language Workbench and should enable DSL designers to detect semantic errors at low cost in the early stages of the design process. We will evaluate the techniques by verifying and testing a representative set of language definitions.

Project Publications

2016

2015

2014

Project Team

  • Eelco Visser (principal investigator)
  • Casper Bach Poulsen (postdoc): verification
  • Daco Harkes (PhD student): case study
  • Hendrik van Antwerpen (PhD student): names and types
  • Opening (PhD student or postdoc)

Other researchers contributing to the project

  • Vlad Vergu (PhD student): DynSem
  • Gabriël Konat (PhD student): Spoofax
  • Eduardo Amorim (PhD student): SDF3
  • Sebastian Erdweg (assistant professor)
  • Andrew Tolmach (Full Professor at Portland State University): verification
  • Peter Mosses (visiting 2016-2017) : semantics specification

Alumni

  • Guido Wachsmuth (assistant professor): NaBL, SDF3, Spoofax
  • Pierre Neron (postdoc): Scope graphs

Open Positions

We are looking for PhD students and postdocs to extend the team. Currently we are advertising for

Contact Eelco Visser for more information about the project or the open positions.

Created April 30, 2013 | Last modified July 8, 2016 | Contributions by Eelco Visser