The Language Designers Workbench: Automating Verification of Language Definitions

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, I 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. I will evaluate the techniques by verifying and testing a representative set of language definitions.