II-NEW: Practical Pluggable Type Systems

该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。有缺陷的软件每年给美国造成高达600亿美元的损失，因此预防缺陷对社会至关重要。 通过运行类型检查器来分析程序以发现给定类型的所有错误，可以防止某些错误。 目前主流编程语言的类型检查器存在着缺陷：有太多的错误无法表达和预防。本项目使程序员能够扩展和定制类型检查器。因此，类型检查器可以检测和预防更多的错误，特别是程序员认为最重要的错误。 其成果包括设计新的类型系统，以解决现实世界的编程问题;一个框架，用于建立自定义类型检查器，在一个工业语言（Java）的背景下;和重要的经验与真正的代码库，以评估的想法，并产生新的研究问题。 该框架将使一个社区的研究人员更迅速和现实地评估他们的理论。 这可能会鼓励更多相关的研究，并对实践产生更大的影响。

This award is funded under the American Recovery and Reinvestment Act of2009 (Public Law 111-5).Buggy software costs the U.S. up to $60 billion annually, so preventingbugs is important to society. It is possible to prevent certain bugs byrunning a type-checker that analyzes a program to find all errors of agiven type. Current type-checkers for mainstream programming languages arelimited: there are too many bugs they cannot express and prevent.This project enables a programmer to extend and customize a type-checker.As a result, the type-checker can detect and prevent more errors, and inparticular the errors that the programmer considers most important. Theoutcomes include design of new type systems for solving real-worldprogramming problems; a framework for building custom type-checkers, in thecontext of an industrial language (Java); and significant experience withreal codebases to evaluate the ideas and to generate new researchquestions. The framework will enable a community of researchers to morequickly and realistically evaluate their theories. This may encourage morerelevant research and lead to more impact on practice.