SHF: Integrating Cost and Behavior in Type Theory

The use of coding assistants, software libraries, and complex hardware continues to simplify software development but makes it increasingly difficult to understand and reason about the efficiency of programs without machine support. However, even in the age of machine-generated code, it is essential to have means of checking that crucial behavioral and cost specifications are met, both to avoid outright correctness bugs and inadvertent inefficiencies that can be difficult to track. Proof assistants are increasingly popular tools for verifying and understanding the behavior of code but the logical foundations of state-of-the-art proof assistants provide little support for reasoning about the efficiency of programs. The project's novelties are to develop a dependent type theory, a foundation for proof assistants, that integrates reasoning about cost and behavior so that correctness and efficiency can be verified in a modular way. The project emphasizes modular decomposition as the central tool for reducing verification cost and permitting reliable code reuse, regardless of whether those components are manually or automatically generated. The project's impacts are to increase the understanding of the efficiency of different implementation strategies both by coding assistants and humans. This can help to better predict the behavior of systems and improve software efficiency, which reduces energy consumption and hardware cost. The project addresses a fundamental shortcoming in the development of mechanically verified software from components: whereas current technology supports cross-module verification of behavior, no extant type theory permits verification of the cost of those components. For practical software development it is essential to permit stating assumptions about the costs of operations in a component to ensure that another component itself obeys given cost requirements, to within various degrees and forms of approximation. Such approximations can be realized with looser or tighter upper bounds, parallel cost accounting, amortization, and probabilistic bounds. The key technical insight is to introduce a phase distinction between the concrete and abstract aspects of a type, which are isolated by modalities. This enables the composition of programs based on interfaces specifying both cost and behavior, allowing for practical development of independent components of a program and reuse of such components in different programs. The proposed work includes the development of the type-theoretic foundations, the integration of automatic cost analyses, the validation of the framework by a (growing) collection of mechanized benchmarks in Agda, and mechanized metatheory and cost-aware compilation. 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 Award ID: 2615896 | Program: 01002627DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Robert Harper | Institution: Carnegie Mellon University, PITTSBURGH, PA | Award Amount: $850,000 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2615896 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2615896.html