权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

SHF: MEDIUM: Performant Sound Gradual Typing

SHF：中：高性能声音渐进打字

基本信息

批准号：
1763922
负责人：
Sam Tobin-Hochstadt
金额：
$ 119.21万
依托单位：
Indiana University
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2018
资助国家：
美国
起止时间：
2018-07-01 至 2023-06-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1763922&HistoricalAwards=false
关键词：
SHF MEDIUM Performant Sound Gradual

项目摘要

Over the past two decades, software developers have switched to a new breed of computer languages. While these languages increase the developers' productivity and allow them to create software for novel devices, they also have the distinct disadvantage of not checking enough safety properties upfront. Failures show up once the software is deployed and may hurt customers. Researchers have recently addressed this problem with the creation of hybrid languages, which embrace rapid production and a way to add safety checks gradually, while industrial developers have developed hybrid languages that omit safety entirely. The project's novelties are about the performance of these hybrid languages, which, as recently discovered, prevent their adoption. If successful, the project's impacts are likely to change the landscape of modern software development on a large scale, adding safety to the most common modern approach to rapid software production.The research project addresses the specific problem of improving the performance of these hybrid languages. While prior research demonstrates that hybrid programming languages are indeed the flexible medium that software developers may want, it also reveals significant performance problems with these languages. The project therefore explores four different ideas of how to eliminate these performance bottlenecks: (1) principled relaxation of the safety guarantees; (2) compiler technology specifically tuned to the additional safety checks; (3) reduction of memory needed for these checks; and (4) application of software verification technology.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

在过去的二十年里，软件开发人员已经转向了一种新的计算机语言。虽然这些语言提高了开发人员的生产力，并允许他们为新设备创建软件，但它们也有明显的缺点，即没有预先检查足够的安全属性。一旦部署软件，故障就会出现，可能会伤害客户。研究人员最近通过创建混合语言来解决这个问题，这种语言支持快速生产和逐渐增加安全检查的方式，而工业开发人员则开发出完全忽略安全性的混合语言。该项目的新奇之处在于这些混合语言的性能，正如最近发现的那样，这些混合语言阻止了它们的采用。如果成功的话，该项目的影响可能会大规模地改变现代软件开发的格局，为最常见的现代快速软件生产方法增加安全性。虽然先前的研究表明，混合编程语言确实是软件开发人员可能想要的灵活媒介，但它也揭示了这些语言的显着性能问题。因此，该项目探讨了四种不同的想法，如何消除这些性能瓶颈：（1）原则上放宽安全保证;（2）编译器技术专门调整到额外的安全检查;（3）减少这些检查所需的内存;以及（4）该奖项反映了NSF的法定使命，并通过评估被认为值得支持使用基金会的知识价值和更广泛的影响审查标准。

项目成果

期刊论文数量（21）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Toward efficient gradual typing for structural types via coercions

通过强制实现结构类型的高效逐步类型化

DOI：
10.1145/3314221.3314627
发表时间：
2019
期刊：
Proceedings of the 40th {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation
影响因子：
0
作者：
Kuhlenschmidt, Andre;Almahallawi, Deyaaeldeen;Siek, Jeremy G.
通讯作者：
Siek, Jeremy G.

Dependent Type Systems as Macros