Rule Formats for Structural Operational Semantics: A Very Short Introduction

Operational semantics describes the behaviour of programs in a language in terms of their execution on an abstract machine, which is often represented as a, possibly infinite, state machine. Structural Operational Semantics is a rule-based and syntax-driven approach to giving operational semantics to programming and specification languages. In this introductory talk, I will discuss some results in the theory of Structural Operational Semantics. These general results aim at ensuring syntactically that (fragments of) programming and specification languages enjoy some desirable semantic property, and are formulated in terms of syntactic templates for operational semantics, called rule formats. The talk will start from first principles and will assume no previous knowledge of the area.