Higher-Order Monad-based Programming and Reasoning

副作用在程序语义和验证中提出了臭名昭著的挑战，这既是因为要考虑的各种影响（例如，以分支类型的形式，如非确定性或概率，各种形式的存储，包括具有动态引用的堆，或高级控制机制），也是因为特定副作用引起的数学复杂性。HOMBRe项目的首要目标是在正确的通用性水平上解决这些挑战，特别是将副作用封装为函数命令式编程范式中的monad，并使用（部分）跟踪的分类概念抽象反馈循环。使用这些原则，我们的目标是开发通用的语义概念，元语言，和高阶验证逻辑的副作用程序和过程在这个意义上。更具体地说，我们将提供方法的语义和逻辑分析的高阶程序与复杂的副作用，如混合（即离散和连续的行为，发现在网络物理系统的混合物）或各种形式的动态引用。治疗这种影响需要进一步发展现有的一般方法。我们将基于语义的循环，不动点，并在我们以前的工作中介绍了保护跟踪的关键概念的反馈，调查特别是图形语言保护的痕迹。此外，我们将设计高级通用验证逻辑，涵盖动态引用和堆等复杂现象，利用我们最近工作中确定的语义结构以及项目中开发的新类别基础。特别是，我们将连接现有的预层语义的动态引用与新设计的模型的基础上名义集，一种形式主义，支持原则和优雅的处理的分配和取消分配的名称，在这种情况下理解为内存位置。在整个项目中，我们将支持在类型论和交互式定理证明器中进行的形式证明所获得的结果，从而不仅增加了对我们结果的形式正确性的信任，而且为在机械化验证中使用它们奠定了基础。

Side effects pose notorious challenges in program semantics and verification, both because of the variety of effects to be taken into account (e.g. in the shape of branching types such as nondeterminism or probability, various forms of store including heaps with dynamic references, or advanced control mechanisms) and because of the mathematical complexity induced by specific side effects. The overarching aim of the HOMBRe project is to tackle such challenges at the right level of generality, in particular encapsulating side effects as monads in the paradigm of functional-imperative programming, and abstracting feedback loops using the categorical concept of (partial) traces. Using these principles, we aim to develop generic semantic concepts, meta-languages, and higher-order verification logics for side-effecting programs and processes in this sense. More specifically, we will provide methods for the semantic and logical analysis of higher-order programs with complex side effects such as hybridness (i.e. a mixture of discrete and continuous behaviour as found in cyber-physical systems) or various forms of dynamic references. The treatment of such effects will require further development of existing generic methods. We will base the semantics of loops, fixpoints, and feedback on the key notion of guarded trace introduced in our previous work, investigating in particular diagrammatic languages for guarded traces. Moreover, we will design advanced generic verification logics covering complex phenomena such as dynamic references and heaps, leveraging semantic structure identified in our own recent work as well as new categorical foundations to be developed in the project. In particular, we will connect the existing presheaf semantics of dynamic references with newly designed models based on nominal sets, a formalism that supports a principled and elegant treatment of the allocation and deallocation of names, in this case understood as memory locations. Throughout the project, we will underpin the results obtained by formal proofs conducted within type theory and interactive theorem provers, thus not only increasing trust in the formal correctness of our results but also paving the ground for using them in mechanized verification.