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）是描述编程语言的含义和行为的形式方法。自动化程序分析、验证、翻译甚至构建都需要这样的方法。SOS 规范描述了程序如何执行操作，同时转换为其他程序。程序可以采取的操作由其子程序的操作决定。这种语义方法很受研究人员的欢迎，许多简单的语言都以这种方式被指定，但是需要一个综合的理论来帮助语言设计者编写结构良好且表现良好的操作语义。我们的目标是这样一个形式化的、数学的SOS理论。我们计划处理操作规范的格式，以保证程序的某些所需属性，提供程序推理的逻辑，实现编程语言之间翻译的推理，并为操作语义的模块化构造提供方法。这样的理论将使编程语言设计者受益，促进新语言的创建、现有语言的修改以及程序的分析。

项目成果

Structural operational semantics for stochastic systems

随机系统的结构操作语义

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