Structuring structural operational semantics

M.R. Mousavi

    Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)

    501 Downloads (Pure)


    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 languageEnglish
    QualificationDoctor of Philosophy
    Awarding Institution
    • Mathematics and Computer Science
    • Groote, Jan Friso, Promotor
    • Plotkin, G.D., Promotor, External person
    • Reniers, Michel A., Copromotor
    Award date26 Sep 2005
    Place of PublicationEindhoven
    Print ISBNs90-386-0644-3
    Publication statusPublished - 2005


    Dive into the research topics of 'Structuring structural operational semantics'. Together they form a unique fingerprint.

    Cite this