Semantics engineering with concrete syntax
Semantics engineering tools like Redex can be used to define, explore, and debug formal definitions of programming language semantics. However, such tools are often based on abstract syntax, which makes the definition of rules and the exploration of execution traces rather unfriendly. In this paper we introduce Credex, a library in the Rascal meta-programming language for defining small-step evaluation-context semantics, where terms and matching patterns are what-you-see-is-what-you-get. Credex employs parsing for decomposing terms into context and redex. Since Rascal’s grammar formalism is based on general parsing, a non-unique decomposition of a term literally corresponds to an ambiguous parse. We demonstrate the use of Credex, detail some aspects of its implementation, and discuss three case-studies.
|, , ,|
|Open Access Series in Informatics|
|Eelco Visser Commemorative Symposium (EVCS) 2023|
|Organisation||Software Analysis and Transformation|
van der Storm, T. (2023). Semantics engineering with concrete syntax. In Eelco Visser Commemorative Symposium (EVCS) 2023 (pp. 29:1–29:11). doi:10.4230/OASIcs.EVCS.2023.29