Structured Operational Semantics
Posted under: Course and Workshop Descriptions; Logic and Computation.
Structured Operational Semantics (SOS) clearly lies in the intersection of Logic and Computation: it is a logical means to define the computational behavior of programs and specifications. SOS was introduced as a systematic way to define operational semantics by a set of deduction rules of a certain shape. SOS has gradually become a de facto standard in formal semantics. Its wide-spread use called for a more fundamental study of SOS and hence SOS rules became the object of study. Several authors syntactically restricted the format of SOS rules and showed several useful properties about the semantics adhering to the format. This has resulted in a line of research proposing various syntactical rule formats and associated meta-theorems.
The goals of this tutorial are
- to introduce the possibilities offered by Structured Operational Semantics in defining formal semantics of languages,
- to get acquainted with the most relevant results in the research field of SOS.
The intended audience consists of graduate students and researchers who would like to use SOS, and researchers who intend to do research in operational semantics.
Material
The tutors will provide lecture notes of approximately 75 pages.
The basic material of the course is inspired by the following textbooks:
Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer. Springer , 2007.
Matthew Hennessy. Semantics of Programming Languages, Wiley, 1990.
Apart from the basic concepts of SOS, presented in the above-mentioned textbooks,
this course puts more emphasis on the logical concepts behind SOS, namely, the model-theoretic and proof-theoretic semantics of SOS.
Moreover, the course gives an overview of the existing results in the SOS meta-theory.
Programme
o Session 1: Introduction (90 minutes)
- Introduction to Formal Semantics (30 minutes)
- History and Raison d’etre of SOS (30 minutes)
- Examples of (simple) SOS specifications: (30 minutes)
o Session 2: Formalizing SOS (90 minutes)
- Formalizing Abstract Syntax (45 minutes)
- Transition System Specifications (45 minutes)
Examples from the literature. Proof- and model-theoretic semantics.
o Session 3: Additional Modeling Primitives (90 minutes)
- Negative Premises (45 minutes)
- Predicates and Structural Congruences (45 minutes)
o Session 4: Design Your Own SOS (90 minutes)
Experience the beauty of SOS by defining the SOS for informally defined languages.
o Session 5: An Overview of SOS Meta-Theory (90 minutes)
Further particulars (e.g, prerequisites): Basic affinity with programming languages and logic (propositional logic, sequent calculus, model theory).
