Mathematical Structural Operational Semantics

Structural operational semantics (SOS) is a formal method of describing the meaning and behaviour of programming languages. Such methods are needed for automated program analysis, verification, translation or even construction.An SOS specification describes how programs can perform actions and, at the same time, transform to other programs. The actions that a program may take are determined by the actions of its subprograms. This semantical method is popular among researchers, and many simple languages have been specified this way, but a comprehensive theory is needed to help language designers write well-structured and well-behaved operational semantics.We aim at such a formal, mathematical theory of SOS. We plan to treat formats for operational specifications that guarantee some desirable properties of programs, provide logics for reasoning about programs, enable reasoning about translations between programming languages, and give means for the modular construction of operational semantics.Such a theory will benefit programming language designers, facilitating the creation of new languages, the modification of existing ones, and the analysis of programs.