Higher-Order Monad-based Programming and Reasoning

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

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.