Foundations of Process Calculi and Contextual Systems

进程演算是一种理想化的语言，旨在对与并发性和移动性相关的各种基础问题进行建模，包括逻辑和物理上的代理的并发性，非确定性和移动性。不幸的是，这种演算的语义非常复杂且高度专业化。由此产生的局部优化的证明方法推理这样的系统，这意味着迄今为止，很难隔离强大的概念和技术。它建议开发一个理论框架，承诺提供统一的理解操作语义和证明技术在广泛的过程语言和模型，旨在捕捉各种现象的并发和移动的计算，以及新兴的过程语言和图形模型的现象，从分子和系统生物学的研究。该框架是表示在语言的范畴理论，重点放在一般性和数学的优雅。它将通过扩展现有的反应系统理论来开发，该理论对过程演算和一般计算形式主义的两个重要特征进行建模：上下文和约简。该理论允许推导出行为良好的标记转换系统，这使得共归纳证明技术的推理上下文等价。通过扩展理论，我们将能够覆盖GUC中出现的更重要的例子，并隔离用于推理其组件的鲁棒证明技术。

Process calculi are idealised languages which aim to model various foundational issues associated with concurrency and mobility, including concurrency, nondeterminism and mobility of agents, both logical and physical. Unfortunately, the semantics of such calculi are very complicated and highly specialised. The resulting local optimisation on the proof methods for reasoning about such systems has meant that it has so far been difficult to isolate robust concepts and techniques. It is proposed to develop a theoretical framework which promises to provide a uniform understanding of operational semantics and proof techniques across a wide range of process languages and models which aim to capture various phenomena of concurrent and mobile computation, as well as emerging process languages and graphical models for the study of phenomena from molecular and systems biology. The framework is to be expressed in the language of category theory, with emphasis placed on generality and mathematical elegance. It shall be developed by extending the existing theory of reactive systems, which model two important features of process calculi and computational formalisms in general: context and reduction. The theory allows the derivation of well-behaved labelled transition systems, which allow coinductive proof techniques for reasoning about contextual equivalence. By extending the theory, we shall be able to cover more significant examples which arise in GUC and isolate robust proof techniques for reasoning about its components.