Mathematical Structural Operational Semantics

数学结构运算语义

• 批准号: EP/D039045/1
• 负责人: Gordon Plotkin
• 金额: $ 15.89万
• 依托单位: University of Edinburgh
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2006
• 资助国家: 英国
• 起止时间: 2006 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FD039045%2F1
• 关键词: 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.

结构操作语义（SOS）是描述编程语言的含义和行为的形式方法。自动化程序分析，验证，翻译甚至构造需要此类方法。AN SOS规范描述了程序如何执行操作以及同时转换为其他程序。程序可能采取的动作取决于其子程序的动作。这种语义方法在研究人员中很受欢迎，并且已经指定了许多简单的语言，但是需要一种全面的理论来帮助语言设计师写出结构性良好的作品，以良好的方式进行操作语义。我们的目标是这种正式的SOS数学理论。我们计划将格式用于操作规格，以保证程序的某些理想属性，提供有关程序的推理的逻辑，能够对编程语言之间的翻译进行推理，并为操作语义的模块化构造提供手段。

项目成果

Structural operational semantics for stochastic systems

随机系统的结构操作语义

• 发表时间: 2008
• 作者: N/a Klin