A Declarative Validator for GSOS Languages
Abstract
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.
Cite
@article{arxiv.2304.06397,
title = {A Declarative Validator for GSOS Languages},
author = {Matteo Cimini},
journal= {arXiv preprint arXiv:2304.06397},
year = {2023}
}
Comments
In Proceedings PLACES 2023, arXiv:2304.05439