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

University Of Pennsylvania, Philadelphia PA

Investigators

Abstract

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.