In my previous talk I described the unfolding of process parameters in mCRL2, as it is done by lpsparunfold.

This technique requires extending data specifications with new operations and equations. As part of the correctness, we need to reason about properties of the data specification. Working on these proofs triggered questions about the mCRL2 data types.

In this talk, I will discuss the progress in my quest for answers to these questions. In particular, what exactly is the semantics of mCRL2 data types, and what are the underlying choices and their motivation (e.g. why do the data types have a model class semantics?)