SOS formats and meta-theory : 20 years after

M.R. Mousavi, M.A. Reniers, J.F. Groote

Research output: Contribution to journalArticleAcademicpeer-review

61 Citations (Scopus)
1 Downloads (Pure)

Abstract

In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS’s) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security-, time- and probability-related issues. In this paper, we provide an overview of SOS rule formats and meta-theorems formulated around them.
Original languageEnglish
Pages (from-to)238-272
JournalTheoretical Computer Science
Volume373
Issue number3
DOIs
Publication statusPublished - 2007

Fingerprint

Structural Operational Semantics
Semantics
Operational Semantics
Transition Systems
Specification
Compositionality
Specifications
Theorem
Programming Languages
Computer Science
Computer programming languages
Computer science
Equivalence
Line
Range of data

Cite this

@article{96132c3e87974140867aab471c6ca467,
title = "SOS formats and meta-theory : 20 years after",
abstract = "In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS’s) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security-, time- and probability-related issues. In this paper, we provide an overview of SOS rule formats and meta-theorems formulated around them.",
author = "M.R. Mousavi and M.A. Reniers and J.F. Groote",
year = "2007",
doi = "10.1016/j.tcs.2006.12.019",
language = "English",
volume = "373",
pages = "238--272",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "3",

}

SOS formats and meta-theory : 20 years after. / Mousavi, M.R.; Reniers, M.A.; Groote, J.F.

In: Theoretical Computer Science, Vol. 373, No. 3, 2007, p. 238-272.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - SOS formats and meta-theory : 20 years after

AU - Mousavi, M.R.

AU - Reniers, M.A.

AU - Groote, J.F.

PY - 2007

Y1 - 2007

N2 - In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS’s) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security-, time- and probability-related issues. In this paper, we provide an overview of SOS rule formats and meta-theorems formulated around them.

AB - In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS’s) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security-, time- and probability-related issues. In this paper, we provide an overview of SOS rule formats and meta-theorems formulated around them.

U2 - 10.1016/j.tcs.2006.12.019

DO - 10.1016/j.tcs.2006.12.019

M3 - Article

VL - 373

SP - 238

EP - 272

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 3

ER -