SHF:Small:Making Effect Systems Practical with Polymorphism, Inference, and Prototyping Support

效果系统是编程语言中类型系统的扩展，它有助于检查程序行为的各个方面，例如它是否安全地使用并发构造，或者是否遵守某些类型的安全策略。最流行的例子是Java编程语言中内置的检查异常的概念。 然而，尽管对效果系统有多年的研究经验，但它们在Java之外并没有广泛使用。 这个项目追求的工作，使效果系统更容易设计，更容易实现，更容易为普通开发人员应用到程序，以防止错误。该项目研究了效果系统的理论，例如如何将它们扩展到异常和生成器等非平凡的编程结构，以及它们的应用。 该项目实现并将各种效果系统应用于Java编写的大量真实世界程序，使用经验评估来指导效果系统理论的改进，特别关注轻量级方法来适应代码重用和效果多态性，而无需开发人员过多的指导。 该项目为特效系统构建了一个开源的实现框架，这将使实现新的特效系统变得更加容易。 该项目通过构建以前提出的Java和新效果系统的开源实现来验证框架，为实践开发人员提供直接有用的工具。 此外，该项目开发了通用推理技术，以自动推断许多效应系统的效应，进一步减少了设计，实施和使用它们所需的工作量。该奖项反映了NSF的法定使命，并被认为是值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估的支持。

Effect systems are extensions to the type system in a programming language that aid in checking aspects of how a program behaves, for example whether it uses concurrency constructs safely, or respects certain kinds of security policies. The most popular example is the notion of checked exceptions built into the Java programming language. Yet despite many years of research experience with effect systems, they are not widely used outside Java. This project pursues work to make effect systems easier to design, easier to implement, and easier for regular developers to apply to programs to prevent bugs. The project investigates both the theory of effect systems, such as how to extend them to non-trivial programming constructs like exceptions and generators, and their application. The project implements and applies a variety of effect systems to substantial real-world programs written in Java, using experience with that empirical evaluation to guide improvements to the theory of effect systems, focusing in particular on lightweight ways to accommodate code reuse and effect polymorphism without requiring excessive guidance from developers. The project constructs an open-source implementation framework for effect systems, which will make it easier to implement new effect systems. The project validates the framework by building open-source implementations of previously proposed and new effect systems for Java, providing tools directly useful to practicing developers. Furthermore, the project develops generic inference techniques to automatically deduce effects for many effect systems, further reducing the effort required to design, implement, and use them.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.