Mathematical Operational Semantics for Data-Passing Processes

操作语义学关注的是通过形式化地描述计算机程序的演化来赋予其意义。如果要证明程序的性质，程序语言的形式化描述是至关重要的。人们可能希望证明一个程序符合规范：例如，它没有安全缺陷;它与其他系统正确交互;或者它计算的值是正确的。当一个人指定一个程序设计语言的操作语义，它通常是必要的证明一些基本性质，以确保推理技术的有效性。这些属性必须为每一个新的语言，被认为是建立，无论何时一个现有的语言是changed.We使用的术语“数学操作语义”（MOS）来描述的过程中理解技术的操作语义在一个抽象的水平。这条研究路线的主要动机是，操作语义学的过程，有时冗长和特设，可以从基本的结构主义观点来理解。第二个更实用的动机是，在这个抽象层次上建立的定理有机会在相当一般的上下文中得到更广泛的应用。考虑到第二个动机，将MOS中的工作视为发生在三个层面上是有帮助的。最高、最抽象和最一般的层次是范畴论的定理，范畴论是以抽象和一般的方式研究数学概念和结构的有力框架。中间层次涉及为特定类型的系统设计范畴理论模型。最低层次是大多数操作语义学家工作的层次，涉及到对特定系统进行推理的特定逻辑框架，我的建议是在这三个层次上都取得进展。我将以数据传递过程演算为例。这些演算是涉及结构化数据的并发和通信的系统的基本编程语言。例如，如果允许通信信道的名称本身被通信，则出现一种移动性。另一种结构化数据涉及加密;涉及这类数据的进程演算已被用于对系统的安全性方面进行建模。在最低的、具体的层面上，所提出的工作涉及从一般结果导出关于数据传递系统的新定理。要做到这一点，有必要研究适合于推理数据传递系统的逻辑框架。这类框架是其他领域的研究人员感兴趣的，比如那些对大型编程系统的形式化感兴趣的人。将被提取的定理将具有以下形式：如果数据传递系统以某种方式指定，则某些属性将保持。这些结果将适用于一般的数据传递系统。他们将被测试对各种语义已经在文献中提出。研究在中间水平将涉及范畴理论模型的数据传递。我将调查现有的模型和结果可以在范畴论域中考虑的程度。这样，数据传递领域将被赋予一个更统一的理论。在最高的抽象层次上，我提出的工作将涉及设计一些复杂证明原则的抽象形式。我将集中讨论两个主题：第一，高阶系统的技术--这些系统可以将程序作为数据接收;第二，我将研究结合证明技术的方法。这项研究将产生一个更好的，更有原则的理解，在这些证明方法所涉及的过程中，并会产生新的，具体的技术，直接相关的操作语义社区。

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.