REU Site: Research Experience for undergraduates in Programming Languages (REPL)

REPL（本科生编程语言研究经验）通过为本科生提供结构化的研究机会来促进下一代编程语言研究。REPL将其学生与宾夕法尼亚大学的编程语言研究小组“PLClub”相结合。在10周内，学生进行前沿研究，掌握相关先决条件，阅读和分析以前的工作，了解正在进行的研究趋势，并学习如何准备有竞争力的博士申请。REPL的重点是提供这些机会，特别是那些在编程语言研究社区中代表性不足的人。2012-2018年间，计算研究协会（CRA）Taulbee的调查显示，在学习编程语言和编译器的计算机科学博士生中，只有4.9%是国内代表性不足的学生。REPL是第一个REU（NSF或其他），专为代表性不足的学生设计，专注于编程语言。 编程语言本身是构建所有现代软件的基本工具，因此研究如何提高编程语言的可靠性、质量和性能对现代计算系统至关重要。REPL研究的重点是有关计算正确性的基本问题。我们如何指定和证明一个程序的正确性？我们如何将这些方法扩展到大型系统？从2015年至2022年，PLClub教师Steve Zdancewic，Benjamin Pierce和Stephanie Weirich共同领导了NSF在计算方面的探险，探索了“深度规范科学”。除此之外，这次探险帮助我们推理了Haskell编程语言、LLVM编译器优化、Web服务器，甚至灯泡控制器的正确性，但还有很多工作要做。灯泡控制软件，就像我们日常使用的许多软件一样，看起来很简单，但完全指定和证明它的行为是正确的却不是。本研究使用形式数学，程序语义学和交互式定理证明器的工具，在这些问题上取得进展。 开发技术以构建高度可信的软件系统是下一代的问题：REPL培训的下一代。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

REPL (Research Experiences for undergraduates in Programming Languages) catalyzes the next generation of programming languages research by providing structured research opportunities for undergraduate students. REPL integrates its students with “PLClub,” Penn’s research group in programming languages. Over 10 weeks, students conduct cutting edge research, master the relevant prerequisites, read and analyze prior work, understand ongoing research trends, and learn how to prepare competitive PhD applications. REPL’s focus is to provide these opportunities especially to those underrepresented in the programming languages research community. Between 2012-2018, the Computing Research Association (CRA) Taulbee survey shows only 4.9% of PhD students in computer science who study programming languages and compilers are domestic underrepresented students. REPL is the first REU (NSF or otherwise) designed for underrepresented students with focus on programming languages. Programming languages themselves are the basic tools by which all modern software is constructed, so studying how to improve the reliability, quality, and performance of programming languages is essential to modern computing systems.REPL research focuses on fundamental questions concerning the correctness of computation. How do we specify and prove the correctness of a program? And how do we make these methods scale to large systems? From 2015-2022, PLClub faculty Steve Zdancewic, Benjamin Pierce, and Stephanie Weirich co-led an NSF Expedition in Computing on these questions that explored the “Science of Deep Specification.” Among other things, the expedition helped us reason about the Haskell programming language, LLVM compiler optimizations, web servers, and even the correctness of a lightbulb controller, yet much is left to do. Lightbulb control software, like much software we use daily, seems simple, but fully specifying and proving that it behaves correctly is not. This research uses the tools of formal mathematics, program semantics, and interactive theorem provers to make progress on these problems. Developing techniques to build highly-trustworthy software systems is a problem for the next generation: the one that REPL trains.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.