A Declarative Validator for GSOS Languages
Matteo Cimini · Electronic Proceedings in Theoretical Computer Science · 2023
Rule formats can quickly establish meta-theoretic properties of process algebras.It is then desirable to identify domain-specific languages (DSLs) that can easily express rule formats.In prior work, we have developed LANG-N-CHANGE, a DSL that includes convenient features for browsing language definitions and retrieving information from them.In this paper, we use LANG-N-CHANGE to write a validator for the GSOS rule format, and we augment LANG-N-CHANGE with suitable macros on our way to do so.Our GSOS validator is concise, and amounts to a few lines of code.We have used it to validate several concurrency operators as adhering to the GSOS format.Moreover, our code expresses the restrictions of the format declaratively.