SHF: SMALL:Dependency Tracking and Dependent Types

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

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.