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.

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