Meta-programming is the activity of writing programs that analyze, create, or transform other programs or models, treating them as data. A large part of software research, but also of science and engineering research in general, relies on transformations or analyses of models – they rely on meta-programming when producing editors, compilers, interpreters, type checkers, code generators, debuggers, refactorings, static analyses, system connectors, and more. We use meta-programming because it helps us to automate tasks previously requiring human involvement. It speeds up research and engineering while maintaining, or even raising quality. Unfortunately, this promise only holds if meta-programs are correct.

Two key use cases for meta-programming are model and program transformations. Transformations are key to compilers and to model-driven engineering. In both areas they are often used by engineers who have limited background in formal reasoning about the transformed objects. The goal of this Dagstuhl Seminar is to consolidate and energize research on automatic static analyses of program and model transformations to help these engineers. We bring together key experts from compiler construction, software verification, model-driven software development, and programming languages to work on this challenge.

Meta-programming is a challenging activity: Meta-programmers must think of all possible input programs for their meta-program while also thinking of all possible inputs to the meta-program's input programs. That is, meta-programmers need to reason about how their meta-programs affect input programs, and how this in turn affects the input program's input and output. For example, a compiler optimization is a meta-program that transforms a program to improve performance. To understand whether an optimization is correct, a meta-programmer shall consider all code fragments to be optimized and all variables occurring in these fragments. Consequently, test cases for such a meta-program encompass both input programs and tests inputs for these programs.

The development processes around designing such software and tools for writing meta-programs exist to a large extent: We have high level program and model manipulation languages (transformation languages, rewrite systems, etc.), specification languages for syntax, we have frameworks for generating editors, we have semantics definition frameworks, and holistic language workbenches that help creating a language deployment fast. However, substantially less work exists on ensuring that the editors, compilers, interpreters, type checkers, code generators, debuggers, etc. are actually correct.

To ensure that meta-programs are correct we need an appropriate set of quality assurance methods and tools. Building programs for analysis and quality assurance of meta-programs is even harder than writing meta-programs. The mechanised correctness proof of the CompCert C compiler is an example of how a meta-program can be guaranteed to be correct but constructing such a proof is a tour de force reserved for experts. Perhaps this is the reason why little effective tooling and methods exist for making meta-programs correct.

It is time to change this. We will address, among others, the three following topics:

• Preservation of semantic properties of transformed models and programs during transformation. A key challenge is to ensure that transformations of programs and models guarantee preservation of some semantic properties. Even, the very notion of semantic properties of objects under transformation is not at clear.
• Inductive Reasoning. A key aspect of meta-programs is usually that they operate on finite, but unbounded input. Language definitions typically involve recursive structures (for instance an expression can nest further expressions). An analyzer for meta-programs needs to construct representations and abstractions for such unbounded data values. We will be discussing possible avenues to obtain such representations.
• Benchmarking. Relatively many examples of transformations and meta-programs can be found in online code repositories and in the literature. Sadly, for most of them the correctness properties are not explicitly formulated. We would like to identify and establish existing known challenge cases for the community to work on.

The seminar will take a highly interactive form, with lightning talks, discussion sessions, working groups, to support starting new research collaborations, projects, as well as collecting and developing case studies, challenges, benchmarks, tools and infrastructure, and obtaining the overview of the field.

Creative Commons BY 3.0 DE

Sebastian Erdweg, Thomas Jensen, Sam Tobin-Hochstadt, and Andrzej Wasowski