A Language Designer's Workbench (AutoSound)
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.
- Eelco Visser (principal investigator)
- Casper Bach Poulsen (postdoc): verification
- Daco Harkes (PhD student): case study
- Hendrik van Antwerpen (PhD student): names and types
- Arjen Rouvoet
Other researchers contributing to the project
- Vlad Vergu (PhD student): DynSem
- Gabriël Konat (PhD student): Spoofax
- Luís Eduardo Souza Amorim (PhD student): SDF3
- Sebastian Erdweg (Assistant Professor)
- Robbert Krebbers (Assistant Professor)
- Andrew Tolmach (Full Professor at Portland State University): verification
- Peter Mosses (visiting since 2016) : semantics specification
- Guido Wachsmuth (assistant professor): NaBL, SDF3, Spoofax
- Pierre Neron (postdoc): Scope graphs
- Michael Steindorfer
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.