SHF: Medium: Collaborative Research: Principled Optimizing Compilation of Dependently Typed Languages
SHF:媒介:协作研究:依赖类型语言的原则优化编译
基本信息
- 批准号:1559983
- 负责人:
- 金额:$ 50.02万
- 依托单位:
- 依托单位国家:美国
- 项目类别:Standard Grant
- 财政年份:2015
- 资助国家:美国
- 起止时间:2015-07-01 至 2018-06-30
- 项目状态:已结题
- 来源:
- 关键词:
项目摘要
Title: SHF: Medium: Collaborative Research: Principled Optimizing Compilation of Dependently Typed LanguagesThe project focuses on a form of software engineering with program verification: writing programs with logical, machine-checkable proofs of correctness, reliability, or security. Such proofs can be done for programs written in conventional programming languages, but the "proof theory" of these languages is complex and difficult, which makes verification time-consuming and expensive. New, "dependently typed" programming languages use principles of functional programming and advanced type systems to achieve a smoother and cleaner proof theory, so that verifying the correctness and safety of software (written in these new languages) is much easier. In this project, the research is to build compilers for these new languages that are efficient and are verified correct.The intellectual merits are in the challenges and opportunities that occur in dependently typed, purely functional contexts, such as the Coq proof assistant. The exciting opportunities that arise only in this context are the ability to choose evaluation order for any sub-term (since Coq's language is pure and total), the ability to open a compiler to user-specified (and certified) rewrite rules that support application-specific optimization, and the ability of programmers to use the Calculus of Inductive Constructions (CiC) proof theory of Coq to verify their programs. The challenges we face, unique to this setting, include the need to determine and erase those terms that are computationally irrelevant. A major foundational challenge is attempting to preserve types (and hence proofs) as we perform lowering transformations, such as conversion to continuation-passing style (CPS) or static single assignment (SSA). Our strategy is to use type and proof-preserving compilation where possible, and where not, to prove a simulation-based notion of correctness. The broader impacts will include (1) pedagogical materials on verified functional programming in Coq; (2) training of graduate students; and (3) improvements in software engineering practice, in enabling practical verified functional programming.
标题:SHF:Medium:协作研究:依赖类型语言的原则性优化编译该项目专注于一种具有程序验证的软件工程形式:编写具有正确性、可靠性或安全性的机器可检查的逻辑证明的程序。用传统编程语言编写的程序可以进行这样的证明,但这些语言的证明理论复杂而困难,这使得验证既耗时又昂贵。新的“依赖类型”编程语言使用函数式编程原理和高级类型系统来实现更流畅、更清晰的证明理论,因此验证软件(用这些新语言编写)的正确性和安全性要容易得多。在这个项目中,研究是为这些新的语言构建高效并被验证正确的编译器。智力的优势在于在依赖类型的纯函数上下文中出现的挑战和机会,例如CoQ证明助手。只有在这种情况下才出现的令人兴奋的机会是能够为任何子项选择求值顺序(因为CoQ的语言是纯的和完全的),能够开放编译器以支持特定于应用程序的优化的用户指定(和认证)重写规则,以及程序员使用CoQ的归纳构造演算(CIC)证明理论来验证他们的程序的能力。我们面临的挑战是这种设置所独有的,包括需要确定和删除那些在计算上不相关的术语。一个主要的基本挑战是在我们执行降级转换时尝试保留类型(从而保留证明),例如转换为延续传递样式(CPS)或静态单一赋值(SSA)。我们的策略是在可能的情况下使用类型和证明保存编译,在可能的情况下,在不可能的情况下,证明基于模拟的正确性概念。更广泛的影响将包括:(1)关于经验证的COQ函数式编程的教学材料;(2)对研究生的培训;(3)改进软件工程实践,使实用的经验证的函数式编程成为可能。
项目成果
期刊论文数量(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 }}
John Morrisett其他文献
John Morrisett的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('John Morrisett', 18)}}的其他基金
SHF: Medium: Collaborative Research: Principled Optimizing Compilation of Dependently Typed Languages
SHF:媒介:协作研究:依赖类型语言的原则优化编译
- 批准号:
1407790 - 财政年份:2014
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
SHF: Small: Collaborative Research: Reusable Tools for Formal Modeling
SHF:小型:协作研究:用于形式建模的可重用工具
- 批准号:
1217891 - 财政年份:2012
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
TC: Large: Collaborative Research: Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software
TC:大型:协作研究:结合基础和轻量级形式方法来构建可证明可靠的软件
- 批准号:
0910660 - 财政年份:2009
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
TC: Small: Collaborative Research: Securing Multilingual Software Systems
TC:小型:协作研究:保护多语言软件系统
- 批准号:
0915030 - 财政年份:2009
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: Integrating Types and Verification
合作研究:整合类型和验证
- 批准号:
0702345 - 财政年份:2007
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
CAREER: Design, Applications, and Foundations of Safe, Low-Level Programming Languages
职业:安全、低级编程语言的设计、应用和基础
- 批准号:
9875536 - 财政年份:1999
- 资助金额:
$ 50.02万 - 项目类别:
Continuing Grant
相似海外基金
Collaborative Research: SHF: Medium: Differentiable Hardware Synthesis
合作研究:SHF:媒介:可微分硬件合成
- 批准号:
2403134 - 财政年份:2024
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: SHF: Medium: Enabling Graphics Processing Unit Performance Simulation for Large-Scale Workloads with Lightweight Simulation Methods
合作研究:SHF:中:通过轻量级仿真方法实现大规模工作负载的图形处理单元性能仿真
- 批准号:
2402804 - 财政年份:2024
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: SHF: Medium: Tiny Chiplets for Big AI: A Reconfigurable-On-Package System
合作研究:SHF:中:用于大人工智能的微型芯片:可重新配置的封装系统
- 批准号:
2403408 - 财政年份:2024
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: SHF: Medium: Toward Understandability and Interpretability for Neural Language Models of Source Code
合作研究:SHF:媒介:实现源代码神经语言模型的可理解性和可解释性
- 批准号:
2423813 - 财政年份:2024
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: SHF: Medium: Enabling GPU Performance Simulation for Large-Scale Workloads with Lightweight Simulation Methods
合作研究:SHF:中:通过轻量级仿真方法实现大规模工作负载的 GPU 性能仿真
- 批准号:
2402806 - 财政年份:2024
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: SHF: Medium: Differentiable Hardware Synthesis
合作研究:SHF:媒介:可微分硬件合成
- 批准号:
2403135 - 财政年份:2024
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: SHF: Medium: Tiny Chiplets for Big AI: A Reconfigurable-On-Package System
合作研究:SHF:中:用于大人工智能的微型芯片:可重新配置的封装系统
- 批准号:
2403409 - 财政年份:2024
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: SHF: Medium: Enabling GPU Performance Simulation for Large-Scale Workloads with Lightweight Simulation Methods
合作研究:SHF:中:通过轻量级仿真方法实现大规模工作负载的 GPU 性能仿真
- 批准号:
2402805 - 财政年份:2024
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: SHF: Medium: High-Performance, Verified Accelerator Programming
合作研究:SHF:中:高性能、经过验证的加速器编程
- 批准号:
2313024 - 财政年份:2023
- 资助金额:
$ 50.02万 - 项目类别:
Standard Grant
Collaborative Research: SHF: Medium: Verifying Deep Neural Networks with Spintronic Probabilistic Computers
合作研究:SHF:中:使用自旋电子概率计算机验证深度神经网络
- 批准号:
2311295 - 财政年份:2023
- 资助金额:
$ 50.02万 - 项目类别:
Continuing Grant