Abstract

Defining a formal (i.e., mathematical) semantics for computer languages is the first step towards developing rigorous techniques for reasoning about computer programs 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.

(Thesis in .pdf format   in .ps format)   Bound paper copy is available upon request.

@PhDThesis{Mousavi05,
    author      = "Mousavi, MohammadReza",
    title       = "Structuring Structural Operational Semantics",
    school      = "Department of Computer Science, Eindhoven University of Technology",
    address     = "Eindhoven, The Netherlands",
    year        = "2005"
}

Back to Publications Page