Axiomatizations from Structural Operational Semantics: Theory and Tools
Eugen-Ioan Goriac · Opin vísindi (Opin vísindi) · 2014
Structural Operational Semantics (SOS) is a well known standard for specifying language semantics in a natural, yet rigorous way. Once a formal way of checking for the equivalence of two programs written in such a language is provided, it is of great interest to derive efficient automated methods to prove if equivalences hold. Also of high interest for language designers is the possibility of enhancing the expressiveness of SOS in a formal manner, preserving as much from the already developed meta-theory of SOS as possible. The thesis focuses on these two areas, both from a theoretical and a practical perspective. The line of research addresses the extension of SOS with predicates and data, while lifting certain results from the meta-theory of SOS to these extensions. These results include automatically deriving axiomatizations for reasoning on program equivalence, and checking for compliance to rule formats in order to guarantee desired properties. Besides these extensions, the thesis provides an axiomatization for the coordination language Linda, presents a method to optimize axiomatizations for language constructs that are commutative, and presents a rule format for idempotent unary operators and idempotent terms. The practical aspect of this thesis consists of a core software framework for working with SOS meta-theories, named MetaSOS, which is implemented in Maude. The framework includes components for automatically deriving axiomatizations, performing simulations, and checking whether language constructs comply to a format for commutativity. It is designed in a modular and extensible fashion, and serves as a base for future implementations of other results from the meta-theory of SOS.