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

通过高级结构中的依赖类型编程推动前沿

• 批准号: 262144-2012
• 负责人: Kahl, Wolfram
• 金额: $ 1.02万
• 依托单位: McMaster University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2015
• 资助国家: 加拿大
• 起止时间: 2015-01-01 至 2016-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=571245
• 关键词: Pushing; Frontier; Dependently; Typed; Programming

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.

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