CAREER: Type-Driven Program Synthesis

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

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.