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.