Mathematical Structural Operational Semantics

结构化操作语义(SOS)是一种描述编程语言的含义和行为的形式化方法。SOS规范描述了程序如何在执行动作的同时转换成其他程序。程序可能采取的操作由其子程序的操作决定。这种语义方法在研究者中很流行，许多简单的语言都是这样描述的，但需要一个全面的理论来帮助语言设计者编写结构良好、行为良好的操作语义。我们致力于这样一种形式化的、数学的SOS理论。我们计划处理保证程序某些理想性质的操作规范的格式，为程序推理提供逻辑，使程序语言之间的翻译推理成为可能，并为操作语义的模块化构造提供手段。这样的理论将有利于编程语言设计者，促进新语言的创建、现有语言的修改和程序的分析。

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.