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.
Original language | English |
---|---|
Qualification | Doctor of Philosophy |
Awarding Institution |
|
Supervisors/Advisors |
|
Award date | 26 Sep 2005 |
Place of Publication | Eindhoven |
Publisher | |
Print ISBNs | 90-386-0644-3 |
DOIs | |
Publication status | Published - 2005 |