Is there a way to add new cases and new functions to existing data types without recompiling the code or sacrificing type safety? The problem is an old problem known as the expression problem. In this discussion, we revisit the problem in the context of theorem proving languages like Coq.

We start by sharing our experience with the expression problem in developing a library for some common structures representing language syntax and semantics. Through the discussion, we would like to learn more about other applications that require solving the expression problem and other people’s experience with the expression problem. Questions for discussion include trade-offs in existing solutions, new solutions, and criteria for new solutions. We hope the discussion will inform future work on the expression problem.

As this is a broad topic, our discussion welcomes people from any kind of background that is related to the expression problem and/or theorem proving. The discussion might also be particularly interesting to people who work on metaprogramming in typed languages, people who work on developing libraries for defining languages, people who want modular proofs for programming languages, and people who have encountered applications that require solving the expression problem in theorem proving.