SHF: SMALL:Dependency Tracking and Dependent Types

University Of Pennsylvania, Philadelphia PA

Investigators

Abstract

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.