Van Horn to Present Paper on Guaranteeing Security and Efficiency in Gradually Typed Programs

Published December 11, 2020

A University of Maryland expert in programming languages is presenting a paper next month that proves it possible to have both soundness and efficiency in a widely used development practice known as gradually typed programs.

David Van Horn, an associate professor of computer science with an appointment in the University of Maryland Institute for Advanced Computer Studies, will share this research at the 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021).

POPL is a forum for the discussion of all aspects of programming languages and programming systems. The event is taking place from January 17–22, 2021, and will be entirely online due to the ongoing COVID-19 pandemic.

“Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification” is concerned with gradual typing, an approach to designing programming languages that can combine the flexibility of dynamically typed languages like Python or JavaScript, with the strong safety guarantees of statically typed languages like Java or OCaml.

Van Horn says this has been an active area of research in the programming languages community for the past 10 years, and has recently gained widespread adoption in all of the largest software companies, with many investing heavily in building their own gradually typed languages.

“The great promise of this work has been that software can be incrementally ported from these more dynamic languages that offer fewer behavior guarantees into components written in more fortified languages, and that programs consisting of a mixture of these components can still offer strong safety guarantees,” he says. “Unfortunately, recent research has borne out that these guarantees come with a prohibitively expensive performance penalty required to monitor the type-based behavior properties imposed on the dynamically typed program components.”

Van Horn notes that this has led to basically all of the industrial gradually typed languages giving up soundness—the important safety guarantees—in exchange for faster run-times.

Van Horn and his team—which includes Cameron Moy, a UMD alumnus who is now a doctoral student at Northeastern University, Phúc (Phil) C. Nguyễn, who received his doctorate in computer science last year, and Sam Tobin-Hochstadt, an associate professor in the School of Informatics & Computing at Indiana University—show in their paper that it is possible to have both soundness and efficiency.

Van Horn says that the basic idea is to examine—in an automated way—the code components written in the dynamic language, and then try to validate the type abstractions imposed upon them using techniques for symbolic execution and automated verification that he and others have been working on.

He says his team evaluated the approach on the original benchmark suite from the paper that first identified the performance problems of gradually typed languages, and found that basically all of the overhead of gradual typing can be eliminated.

“This means that programmers can enjoy the added engineering benefits of strong semantic guarantees and pay basically no run-time cost to enforce them,” Van Horn says.

—Story by Melissa Brachfeld