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.

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