Mathematical Operational Semantics for Data-Passing Processes

数据传递过程的数学运算语义

基本信息

批准号：
EP/E042414/1
负责人：
Samuel Staton
金额：
$ 26.66万
依托单位：
University of Cambridge
依托单位国家：
英国
项目类别：
Fellowship
财政年份：
2007
资助国家：
英国
起止时间：
2007 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FE042414%2F1
关键词：
Mathematical Operational Semantics Data Passing

项目摘要

Operational semantics is concerned with ascribing meaning to computer programs by formally describing their evolution. A formal description of a programming language is crucial if one is to prove properties of programs. One may wish to prove that a program meets a specification: for instance, that it has no security flaws; that it interacts correctly with other systems; or that the values it computes are correct. When one specifies an operational semantics for a programming language, it is usually necessary to prove some basic properties in order to ensure the validity of reasoning techniques. These properties have to be established for every new language that is considered, and whenever an existing language is changed.We use the term 'Mathematical Operational Semantics' (MOS) to describe the process of understanding techniques from operational semantics at an abstract level. A primary motivation for this line of research is that procedures from operational semantics, at times lengthy and ad hoc, can be understood from a basic structuralist viewpoint. A second, more pragmatic motivation is that theorems that are established at this abstract level have the chance of wider application in quite general contexts. With this second motivation in mind, it is helpful to see work in MOS as occuring at three levels. The highest, most abstract and general level, is concerned with theorems of category theory, which is a powerful framework for studying mathematical concepts and structures in an abstract and general way. The intermediate level involves devising category-theoretic models for particular kinds of system. The lowest level is the level at which most operational semanticists work, and involves particular logical frameworks for reasoning about particular systems.My proposal is to make progress at all three of these levels. I will take, as a case study, the data-passing process calculi. These calculi are basic programming languages for systems that involve concurrency and communication of structured data. For instance, if one allows the names of communication channels to themselves be communicated, then a kind of mobility arises. Another kind of structured data involves encryption; process calculi involving this kind of data have been used to model security aspects of systems.At the lowest, concrete level, the proposed work involves deriving new theorems about data-passing systems from the general results. To do this it will be necessary to investigate logical frameworks that are suitable for reasoning about data-passing systems. Frameworks of this sort are of interest to researchers in other fields, such as those interested in the formalisation of large scale programming systems. Theorems that will be extracted will be of the form: if a data-passing system is specified in a certain way, then certain properties will hold . The results will hold for data-passing systems in general. They will be tested against various semantics that have been proposed in the literature.Research at the intermediate level will involve category-theoretic models of data-passing. I will investigate the extent to which existing models and results can be considered in the category-theoretic domain. In this way the field of data-passing will be given a more unified theory.At the highest level of abstraction, my proposed work will involve devising abstract forms of some complex proof principles. I will focus on two topics: firstly, techniques for higher-order systems -- these are systems that can receive programs as data; secondly, I will investigate ways of combining proof techniques. This research will give rise to a better, more principled understanding of the processes involved in these proof methods, and will give rise to new, concrete techniques of immediate relevance to the operational semantics community.

操作语义与正式描述其演变有关将含义归因于计算机程序的意义。如果要证明程序的属性，对编程语言的正式描述至关重要。一个人可能希望证明一个程序符合规范：例如，它没有安全缺陷；它与其他系统正确交互；或者它计算的值是正确的。当人们为编程语言指定操作语义时，通常有必要证明一些基本属性，以确保推理技术的有效性。这些属性必须为所考虑的每种新语言建立，并且每当更改现有语言时。我们使用“数学操作语义”（MOS）一词来描述从抽象层面上从操作语义中理解技术的过程。这一研究的主要动机是，从基本的结构主义观点可以理解操作语义的程序，有时可以漫长而临时。第二，更务实的动机是，在此抽象层面上建立的定理具有在相当一般的环境中更广泛的应用。考虑到第二个动机，将MOS的工作视为三个级别的工作是有帮助的。最高的，最抽象和一般的层面与类别理论的定理有关，这是以抽象和一般方式研究数学概念和结构的有力框架。中级级别涉及为特定类型的系统设计类别理论模型。最低级别是大多数操作语义学家工作的水平，并且涉及特定的逻辑框架来推理特定系统。我的建议是在这三个级别上取得进展。作为案例研究，我将采用数据通过的计算。这些结石是涉及结构化数据并发和通信的系统的基本编程语言。例如，如果允许传达通信渠道的名称，则会出现一种移动性。另一种结构化数据涉及加密。涉及这种数据的过程计算已用于建模系统的安全性方面。在最低的具体级别上，提出的工作涉及从一般结果中得出有关数据通信系统的新定理。为此，有必要研究适合推理数据通信系统的逻辑框架。其他领域的研究人员（例如那些对大规模编程系统的形式化感兴趣的研究人员）感兴趣的框架。将提取的定理将是形式：如果以某种方式指定数据通信系统，则某些属性将保持。总体上，结果将适用于数据通行系统。它们将针对文献中提出的各种语义进行测试。中级研究将涉及数据通信的类别理论模型。我将研究可以在类别理论领域中考虑现有模型和结果的程度。通过这种方式，数据通行的领域将得到更加统一的理论。在最高的抽象水平，我提出的工作将涉及设计一些复杂的证明原则的抽象形式。我将重点介绍两个主题：首先是高阶系统的技术 - 这些系统可以接收程序作为数据；其次，我将研究结合证明技术的方法。这项研究将产生对这些证明方法所涉及的过程的更好，更有原则的理解，并引起与操作语义社区直接相关的新型具体技术。