CAREER: Extensibility in Theory and Practice

点击翻译按钮获取中文摘要

Modern software engineering relies on large ecosystems of independent software components and libraries. This poses two challenges for the design of programming languages and language tooling, both of which are addressed by this project. First, languages must support developing independent components, including identifying and abstracting reusable components from existing applications. Second, languages must provide expressive specification mechanisms to ensure that components are used correctly and that components do not have unintended interactions. The project's novelties are new programming language features for modular specification and implementation of program data and behavior, at all level of the software stack from user-facing applications to operating system components and hardware support. The project's impacts are improvements in both software reliability and programmer productivity, as the project enables language tooling to automatically help programmers identify and correctly use software components and libraries.The project has two primary themes. The first is modularity and reuse in high-level functional programs. The project develops extensible types for data and computational effects, supporting high-level abstractions including overloading, generic programming, and extensible effect handlers. The second is modularity and reuse in low-level and systems programs. The project develops extensible bit-level specifications of data structures and their layout, targeting applications including operating system kernels and hardware interfaces. Each of these themes will only have impact if the resulting language features have comparable performance with existing approaches. The project uses linear typing and compile-type specialization to offset runtime costs traditionally associated with generic and extensible programming techniques.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.