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.