SHF: SMALL:Dependency Tracking and Dependent Types

SHF：SMALL：依赖性跟踪和依赖性类型

• 批准号: 2327738
• 负责人: Stephanie Weirich
• 金额: $ 54万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-12-01 至 2026-11-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2327738&HistoricalAwards=false
• 关键词: SHF; SMALL; Dependency; Tracking; Dependent

The overarching goal of this project is to improve the expressiveness of dependently-typed programming language. The project's novelties are the use of dependency tracking as a mechanism for extending existing type systems with new capabilities. These new type systems will form the basis for the extensions of existing programming languages and the designs of future ones. The project's impact will be to increase the expressiveness of the development time checking performed by programming environments during software construction. Dependent type systems offer significant promise as a component of software developer's toolbox. However, their integration into the programming process is not without difficulties. This project addresses several issues that arise in the context of this design, including efficient compilation, expressiveness, and amenability to automation. Broader impacts of the project include lectures at the NSF-supported Oregon Programming Languages Summer School; collaborations with type system designers in industry; and talks at industrial venues and developer conferences. Contributions to Broadening Participation in Computing are achieved through training a diverse cohort of undergraduate students in a departmental Research Experiences for Undergraduates (REU) Sites project.The project will investigate the integration of dependency tracking with dependent type systems. In particular, it will explore how this mechanism can be applied to the design of dependently-typed programming languages and study how the features of dependently-typed programming languages can enable more expressive forms of type-based dependency analysis. In particular, this project targets applications of dependency analysis designed to track relevance, termination, decidability, and data structure layout. The results of each of these analyses benefit the development of dependently- typed programs, making them faster, safer, more automatic and easier to compile. The type systems developed during the course of this project will be rigorously evaluated through the creation of mechanical proofs of correctness and through experiments with an implementation of the novel type system. All proofs and software produced in the course of the project will be made publicly available.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.

该项目的总体目标是提高依赖类型编程语言的表达能力。该项目的新颖之处在于使用依赖项跟踪作为一种机制，通过新功能扩展现有类型系统。这些新型类型系统将构成现有编程语言的扩展和未来编程语言的设计的基础。该项目的影响将是提高软件构建期间编程环境执行的开发时间检查的表现力。 依赖类型系统作为软件开发人员工具箱的一个组件提供了重要的前景。然而，将它们集成到编程过程中并非没有困难。该项目解决了该设计中出现的几个问题，包括高效编译、表达能力和自动化的适应性。该项目的更广泛影响包括在 NSF 支持的俄勒冈州编程语言暑期学校的讲座；与行业类型系统设计师的合作；以及在工业场所和开发者会议上的演讲。通过在本科生研究体验 (REU) 站点项目中培训不同的本科生群体，可以为扩大计算参与做出贡献。该项目将研究依赖跟踪与依赖类型系统的集成。特别是，它将探索如何将这种机制应用于依赖类型编程语言的设计，并研究依赖类型编程语言的特性如何能够实现更具表现力的基于类型的依赖分析。 特别是，该项目的目标是依赖性分析的应用程序，旨在跟踪相关性、终止性、可判定性和数据结构布局。这些分析的结果都有利于独立类型程序的开发，使它们更快、更安全、更自动化且更容易编译。在该项目过程中开发的类型系统将通过创建正确性的机械证明以及通过实施新型类型系统的实验来严格评估。该项目过程中产生的所有证据和软件都将公开。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。