SHF: SMALL:Dependency Tracking and Dependent Types

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

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.