Topics in Structural Operational Semantics
My MSc thesis presents three papers, each using SOS in their own way.
Abstract: Structural Operational Semantics (SOS) provides a mathematically rigourous way of specifying the semantics of formal (programming) languages. This thesis presents three individual contributions which highlight different uses of SOS and demonstrate how it may be used to benefit computer science. Together, the topics span a relatively wide spectrum, but their common theme is their use of SOS although each topic contains its own scientific contribution as well. In order, the topics range from practical applications of SOS to abstract meta-theory reasoning about SOS rules at a higher level.
The first contribution relates to the use of operational semantics to specify the behaviour of a policy enforcement architecture built on top of transactional memory in Haskell. The second one discusses work in constructing a method for compositional reasoning about process calculi that includes a representation of the history of a computation, and allows the specification logic to look into the past. The final topic looks at SOS at a higher level, where we develop a rule format, which is a syntactic constraint on SOS rules that guarantees certain properties about the operators they define, namely determinism and idempotency.
