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.
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.
- Intrinsically Typed Definitional Interpreters for Imperative Languages (POPL 2018)
- Towards Zero-Overhead Disambiguation of Deep Priority Conflicts (Programming 2018)
- PixieDust: Declarative Incremental User Interface Rendering through Static Dependency Tracking (WWW 2018)
- IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition (ECOOP 2017) [(Artifact)]
- Deep priority conflicts in the wild: a pilot study (SLE 2017)
- The Semantics of Name Resolution in Grace (DLS 2017)
- Scopes describe Frames: A uniform model for memory layout in dynamic semantics (ECOOP 2016)
- A constraint language for static semantic analysis based on scope graphs (PEPM 2016)
- IceDust: Incremental and eventual computation of derived values in persistent object graphs (ECOOP 2016)
- Principled syntactic code completion using placeholders (SLE 2016)
- A theory of name resolution (ESOP 2015)
- Understanding software through linguistic abstraction (SCP)
- DynSem: A DSL for Dynamic Semantics Specification (RTA 2015)
- A language designer’s workbench: A one-stop-shop for implementation and verification of language designs (Onward! 2014)
- Unifying and generalizing relations in role-based data modeling and navigation (SLE 2014)
- 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