Pushing the Frontier with Dependently Typed Programming in High-Level Structures

这项研究的目标是利用数学抽象来改进软件重用，并提高软件开发人员在涉及深度嵌套结构的复杂转换的软件开发中的生产力和信心，例如在高性能计算的代码生成中需要它们。 众所周知，在许多应用领域，特别是在涉及任何类型的网络的情况下，简明的关系-代数规范可用于许多任务。这项研究将开辟一种新的方法来结合规范和编程来针对这些关系代数接口，以一种确保正确性属性的组合性的方式。这将通过使用依赖类型编程的新范例来实现，并以一种直接利用其主要优势的方式使用它，即提供一种自然而精确的方式来表达严格的数学定义。这样，我们将能够以模块化的方式指定新的转换概念，这些概念涉及在深度嵌套的结构中跨几个抽象级别移动组件，例如表示并发多核程序的组合控制流图和数据流图。相关的经验证的实现构建块将单独地为人类理解所访问，这为将以可证明的安全方式组成和导出的高度复杂的实现提供必要的验证，以执行用传统方法几乎不可能自信地开发的符号操作。 这种对复杂优化技术进行规范和编程的统一方法将使它们也可用于越来越多的应用领域，其中软件用于安全关键环境，因此必须认证为正确。作为实际应用，本研究产生的嵌套代码图转换能力将目标是生成用于医学成像的经过机械验证的高性能代码。

The goal of this research is to leverage mathematical abstractions to improve software reuse, and to increase software developers' productivity and confidence in the development of software involving complex transformations of deeply nested structures, as they are needed for example in code generation for high-performance computing. It is well-known that in many application areas, in particular where networks of any kind are involved, concise relation-algebraic specifications are available for many tasks. This research will open up new ways to combine specification and programming against these relation-algebraic interfaces in a way that ensures compositionality of correctness properties. This will be achieved by using the novel paradigm of dependently-typed programming, and employing it in a way that directly leverages its main strength of providing a natural and precise way to express rigorous mathematical definitions. With this, we will able to specify, in a modular way, novel transformation concepts that involve moving components across several levels of abstraction in deeply nested structures representing for example combined control- and data-flow graphs of concurrent multi-core programs. The associated verified implementation building blocks will individually be accessible to human understanding, which provides essential validation to the highly complex implementations that will be composed and derived in a certifiably safe manner to perform symbolic manipulations that would be almost impossible to confidently develop with conventional approaches. This unified approach to specification and programming of complex optimisation techniques will make them available also to the increasingly many application areas where software is used in safety-critical environments, and therefore must be certified as correct. As a practical application, the nested code graph transformation capabilities produced by this research will target generation of mechanically verified high-performance code to be used in medical imaging.