CAREER: Type-Driven Program Synthesis

自动化编程的低级方面以帮助开发人员提高生产力并避免错误变得越来越重要。程序综合是一种新兴的技术，用于从程序必须执行的任务的高级描述中自动生成程序。使程序合成实用化需要解决两个主要的挑战：（1）程序员应该如何将他们的意图传达给合成器？以及（2）如何有效地搜索合成器需要考虑的所有节目的空间？类型驱动合成项目（TyDriS）使用一种新的基于类型的方法来解决这两个挑战，该方法利用了编程语言社区在类型系统上数十年的工作，以利于程序合成。为了应对规范的挑战，TyDriS提供了强大的语言，允许程序员非常简洁地传达大量信息，即使在存在歧义的情况下也能获得相关结果。面对规模的挑战，TyDriS贡献了新的搜索算法，允许综合利用大型代码库，并将合成代码与程序员编写的代码集成在一起。这些创新使三个新的应用程序：基于库的Haskell合成器，隐私意识的Web框架，和合成辅助编程tutor.This奖项反映了NSF的法定使命，并已被认为是值得通过评估使用基金会的智力价值和更广泛的影响审查标准的支持。

It is becoming increasingly important to automate low-level aspects of programming to help developers increase productivity and avoid mistakes. Program synthesis is an emerging technology for automatically generating programs from high-level descriptions of the task they must perform. Making program synthesis practical requires addressing two major challenges:(1) how should the programmer communicate their intent to the synthesizer? and (2) how does one efficiently search the space of all programs the synthesizer needs to consider?The Type-Driven Synthesis project (TyDriS) tackles both of these challenges using a novel type-based approach, which leverages decades of work on type systems from the Programming Languages community for the benefit of program synthesis. Towards the challenge of specification, TyDriS contributes powerful languages that allow the programmer to communicate a lot of information very concisely, and get relevant results even in the presence of ambiguity. Towards the challenge of scale, TyDriS contributes new search algorithms that allow synthesis to leverage large code libraries and integrate synthesized code with programmer-written code. These innovations enable three novel applications: a library-based synthesizer for Haskell, a privacy-aware web framework, and a synthesis-aided programming tutor.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.