Higher-Order Monad-based Programming and Reasoning

点击翻译按钮获取中文摘要

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.