CSE researchers receive Distinguished Paper Award at OOPSLA 2023

October 27, 2023
CSE authors were recognized for the excellence of their research on live pattern matching with typed holes in modern programming systems.
A computer screen against a maize background with overlapping programming text showing the syntax of Peanut as well as examples of pattern matching with holes.

A team of CSE researchers has received a Distinguished Paper Award at the 2023 Object-oriented Programming, Systems, Languages, and Applications (OOPSLA) conference for their paper titled “Live Pattern Matching with Typed Holes.” The authors include recent CS graduates Yongwei Yuan, Scott Guest, and Hannah Potter; CSE PhD students Eric Griffis and David Moon; and Prof. Cyrus Omar.

OOPSLA is hosted by the ACM Special Interest Group on Programming Languages (SIGPLAN) and is part of the International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH). OOPSLA is a top international conference which brings together experts in programming languages and software engineering to network and share the latest findings in these areas. This year’s conference took place in Lisbon, Portugal from October 25-27, 2023.

Papers honored with the OOPSLA Distinguished Paper Award, only a select few of those presented at the conference, are chosen based on their outstanding quality and significance to the field.

Two columns showing the syntax of Peanut, including type and rules.
Syntax of Peanut. Here, n ranges over mathematical numbers (of any suitable sort),  x over variables, u over expression hole names, and w over pattern hole names.

In their paper, Yuan et al. examine the phenomenon of typed holes, an increasingly common feature of modern programming systems that allows holes to be used as expressions. This approach enables greater flexibility and dynamism during program development, including real-time feedback and assistance.

Previously, such holes were only used in types and expressions; CSE researchers have taken this technique a step further by exploring its application in patterns. They first examined the primary problems posed by typed pattern holes, including how to ensure exhaustiveness and avoid redundancy in patterns that are not fully known, as well as how to perform real-time evaluation of both expression and pattern holes.

Examples of exhaustiveness checking with pattern holes, including indeterminately exhaustive checking, necessarily inexhaustive checking, and necessarily exhaustive checking.
Examples of exhaustiveness checking with pattern holes.

To this end, the researchers developed Peanut, a typed lambda calculus that addresses the problems of exhaustiveness and redundancy and leverages operational semantics to enable live evaluation of holes in both expressions and patterns. The team then implemented Peanut in the programming environment Hazel, which automatically inserts holes during editing, making it the first general-purpose functional language with real-time feedback for programmers.

This research constitutes a considerable advance in the design of dynamic programming environments with real-time evaluation and opens up new avenues for development in this area.