Towards "Mouldable Code" as a Better Approach to Synthesis of Efficient and Correct Software
将“可塑代码”作为合成高效、正确软件的更好方法
基本信息
- 批准号:RGPIN-2017-05684
- 负责人:
- 金额:$ 1.46万
- 依托单位:
- 依托单位国家:加拿大
- 项目类别:Discovery Grants Program - Individual
- 财政年份:2020
- 资助国家:加拿大
- 起止时间:2020-01-01 至 2021-12-31
- 项目状态:已结题
- 来源:
- 关键词:
项目摘要
Important parts of the supporting infrastructure for optimising code generators, in particular in compilers, consist of analyses of graphs, especially control-flow graphs and data-flow graphs. In addition, many of the optimisations enabled by these analyses are usefully understood as graph transformations.
Interestingly, the program transformation literature almost exclusively concentrates on transformation of (higher-order) abstract syntax trees. This corresponds to the usual approach in a compiler context to first parse the given programs into abstract syntax trees, and then extract from these the necessary information to construct the graphs to be used for data-flow and control-flow analyses, while still considering the abstract syntax trees as the internal representation of the program.
However, many of the transformations that are used for code optimisation, in particular in the back-ends of compilers, act on patterns that can usefully be thought of as graph patterns, and the resulting transformations are frequently explained in the literature as graph transformations applied to control-flow graphs and data-flow graphs.
In this research programme, I aim to create the theoretical justifications for control-flow graph transformation and data-flow graph transformations by linking the theories of control-flow and data-flow semantics with appropriate theories of graph transformation and build on these foundations a mechanised framework for nested code graph transformation.
The goal of this framework is to be the first representative of a new class of mechanised environments in which experts can design special-purpose optimisation passes in a graph-based formalism that captures the intuitive graph-based descriptions of optimisation passes as they are customary in the compiler literature. However, while the graph-based descriptions in the literature are technically completely informal, the envisaged mechanised system will support not only capturing the design itself, but also proving the correctness of these optimisations at a level that is conceptually close to the design, and will finally also automatically generate correct-by-construction implementations of these optimisation passes.
优化代码生成器(特别是编译器中的代码生成器)的支持基础结构的重要部分由图的分析组成,特别是控制流图和数据流图。此外,通过这些分析实现的许多优化可以被理解为图形转换。
项目成果
期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
数据更新时间:{{ journalArticles.updateTime }}
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
Kahl, Wolfram其他文献
Kahl, Wolfram的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('Kahl, Wolfram', 18)}}的其他基金
Towards "Mouldable Code" as a Better Approach to Synthesis of Efficient and Correct Software
将“可塑代码”作为合成高效、正确软件的更好方法
- 批准号:
RGPIN-2017-05684 - 财政年份:2021
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Towards "Mouldable Code" as a Better Approach to Synthesis of Efficient and Correct Software
将“可塑代码”作为合成高效、正确软件的更好方法
- 批准号:
RGPIN-2017-05684 - 财政年份:2019
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Towards "Mouldable Code" as a Better Approach to Synthesis of Efficient and Correct Software
将“可塑代码”作为合成高效、正确软件的更好方法
- 批准号:
RGPIN-2017-05684 - 财政年份:2018
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Towards “Mouldable Code” as a Better Approach to Synthesis of Efficient and Correct Software
将“可塑代码”作为合成高效、正确软件的更好方法
- 批准号:
RGPIN-2017-05684 - 财政年份:2017
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Pushing the Frontier with Dependently Typed Programming in High-Level Structures
通过高级结构中的依赖类型编程推动前沿
- 批准号:
262144-2012 - 财政年份:2016
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Pushing the Frontier with Dependently Typed Programming in High-Level Structures
通过高级结构中的依赖类型编程推动前沿
- 批准号:
262144-2012 - 财政年份:2015
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Pushing the Frontier with Dependently Typed Programming in High-Level Structures
通过高级结构中的依赖类型编程推动前沿
- 批准号:
262144-2012 - 财政年份:2014
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Pushing the Frontier with Dependently Typed Programming in High-Level Structures
通过高级结构中的依赖类型编程推动前沿
- 批准号:
262144-2012 - 财政年份:2013
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Pushing the Frontier with Dependently Typed Programming in High-Level Structures
通过高级结构中的依赖类型编程推动前沿
- 批准号:
262144-2012 - 财政年份:2012
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Tool support for relational formalisms in programming and specification
编程和规范中关系形式主义的工具支持
- 批准号:
262144-2007 - 财政年份:2011
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
相似海外基金
Towards "Mouldable Code" as a Better Approach to Synthesis of Efficient and Correct Software
将“可塑代码”作为合成高效、正确软件的更好方法
- 批准号:
RGPIN-2017-05684 - 财政年份:2021
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Towards "Mouldable Code" as a Better Approach to Synthesis of Efficient and Correct Software
将“可塑代码”作为合成高效、正确软件的更好方法
- 批准号:
RGPIN-2017-05684 - 财政年份:2019
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Investigation of methods and materials for individually mouldable micro-stereotactic frame
可单独成型的微立体框架的方法和材料研究
- 批准号:
433571394 - 财政年份:2019
- 资助金额:
$ 1.46万 - 项目类别:
Research Grants
Towards "Mouldable Code" as a Better Approach to Synthesis of Efficient and Correct Software
将“可塑代码”作为合成高效、正确软件的更好方法
- 批准号:
RGPIN-2017-05684 - 财政年份:2018
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Towards “Mouldable Code” as a Better Approach to Synthesis of Efficient and Correct Software
将“可塑代码”作为合成高效、正确软件的更好方法
- 批准号:
RGPIN-2017-05684 - 财政年份:2017
- 资助金额:
$ 1.46万 - 项目类别:
Discovery Grants Program - Individual
Mouldable Auto Parts From Sustainable Resources
来自可持续资源的可模制汽车零部件
- 批准号:
100530 - 财政年份:2008
- 资助金额:
$ 1.46万 - 项目类别:
Collaborative R&D