CSE researchers win Distinguished Paper Award at POPL 2024

Researchers in CSE have won a Distinguished Paper Award at the 2024 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) for their paper titled “Total Type Error Localization and Recovery with Holes.” Authors on the paper include Prof. Cyrus Omar, who leads the Future of Programming Lab at Michigan, undergrad and lead author Eric Zhao, PhD student Andrew Blinn, and recent alums Anand Dukkipati, Raef Maroof, and Zhiyi Pan.

POPL is a top conference in programming languages, bringing together practitioners and researchers at the forefront of the field to share new developments and ideas in this area. The Distinguished Paper Award is given to just a small fraction of papers at the conference and seeks to recognize outstanding, impactful research. 

CSE authors received the award in recognition of their development of  the marked lambda calculus, a formal model of how to locate and recover from type errors in program expressions.

A type system is a set of rules for how to distinguish between expressions of different types, e.g., integers from functions. Many programming languages have type systems because they allow the system to discover inconsistencies between the expected type and the actual type of the code that the programmer has inserted. When there are no such inconsistencies, type systems support efficient program compilation and rich program analysis.

Given the central role of type systems in programming, type error localization and recovery is an important practical concern—users don’t want program compilation and execution to fail silently when there is a problem. Previously, language implementations approached this important problem in an ad hoc manner that differed widely between different language implementations. 

Seeking to create a more efficient and holistic remedy to this problem, CSE researchers have developed a principled method, embodied into a formal language called the marked lambda calculus, that achieves a property called totality: there are no situations in which the system cannot recover from an error. This property is particularly critical for large programs, where there may be errors throughout over long periods of development, during which programmers still expect helpful feedback from their programming environment no matter what part of the program they are working with. In their paper, the researchers used an automated theorem power, which allows a computer to check that the mathematical proofs are correct, to establish totality and other important properties, 

Going further, the paper develops a system for integrating type inference into the system where, again, inference errors do not cause inference to fail outright but rather to localize the problem to unfillable type holes, i.e., places where a type is needed but cannot be inferred. The programmer themselves can then decide from partial solutions to the inference problem, at which point control returns to the marking system described above.

These ideas have been implemented in Hazel, a new programming environment being developed in Omar’s lab that maintains liveness, meaning that there is no traditional edit-compile-run development, which leads to delayed feedback. Instead, feedback is rapid and detailed, which is known to improve the programming experience. Hazel is already being used to teach in courses at U-M.

“Our hope is that Hazel will pave the way for not only better programs but also a better programming experience,” said Omar, “particularly as we move toward a more collaborative, global model of computing where nothing is ever truly complete and error-free.”