Structuring structural operational semantics

Abstract

Defining a formal (i.e., mathematical) semantics for computer languages is the first step towards developing rigorous techniques for reasoning about computerprograms and specifications in such a language. Structural Operational Semantics (SOS), introduced by Plotkin in 1981, has become a popular technique for defining formal semantics. In this thesis, we first review the basic concepts of SOS and the existing meta-results. Subsequently, we enhance the state of the art in this field by offering the following contributions:• developing a syntactic format guaranteeing a language construct to be commutative;• extending the existing congruence and well-definedness meta-results to the setting with equational specifications;• defining a more liberal notion of operational conservativity, called orthogonality,and formulating meta-theorems for it;• prototyping a framework for checking the premises of congruence and conservativity meta-theorems and animating programs according to their SOS specification;• defining notions of bisimulation with data and formulating syntactic rule formats guaranteeing congruence for these notions;• proposing syntactic rule formats for guaranteeing congruence of strong bisimilarity and higher-order bisimilarity in the setting of higher order processes.