The Lab for Programming Languages at the University of Maryland (PLUM) is engaged in exciting research that aims to improve software quality through new languages and software tools. Our work involves formalism and proof (e.g., to show that a particular analysis establishes a certain property of the programs it considers) as well as implementation and evaluation (e.g., to show that our ideas work on real software at reasonable cost). Current interests focus on formal verification, type systems, gradual typing and contracts, quantum programming languages, property-based testing, functional programming, program synthesis, static analysis, information flow control, privacy-preserving computation, and high-availability systems.
News
Alp’s Programmable Property-Based Testing paper won a Distinguished Paper Award at ICFP 2026!
One PLUM-authored paper will appear at SPLASH 2026: Testing Theorems, Fully Automatically, by Segev Elazar Mittelman, with Harrison Goldstein, and Leonidas Lampropoulos.
The experience report Evaluating Shrinking, authored by Alperen Keles, with George Miao, and Leonidas Lampropoulos, will appear at the Haskell Symposium.
One PLUM-authored paper will appear at ICFP 2026: Programmable Property-Based Testing, led by Alperen Keles, with Justine Frank, Harrison Goldstein, and Leonidas Lampropoulos.
Milijana Surbatovich has been awarded a National Science Foundation CAREER Award for her project titled Formally Verified Intermittent Systems with Tiered Trust. The project aims to make emerging intermittent computing platforms safe and reliable for applications with strict correctness and security requirements. The research will develop foundational models, programming languages, and machine-verified tools to ensure embedded systems continue to operate correctly despite unavoidable power failures, with potential impact across biomedical devices, disaster monitoring, and defense applications. (Read more.)
David Van Horn will lecture at the Cornell, Maryland, Max Planck Pre-doctoral Research School in Saarbrücken, August 3-7. The lectures will use gradual typed programming languages as a vehicle for introducing core methods in programming language research, including formal syntax, operational semantics, type systems, and associated proof techniques and tools such as proof assistants.
The paper DIRT: Database-Integrated Random Testing by Alperen Kelles, Ethan Chou, Harrison Goldstein, and Leonidas Lampropoulos, will appear at DBTest 2026.
Two papers co-authored by PLUM members will appear at PLDI 2026: Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow by Zhengyao Lin, Yi Cai, and Milijana Surbatovich; and The Search for Constrained Random Generators by Harrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati, Leonidas Lampropoulos, and Benjamin Pierce.
One paper co-authored by PLUM members will appear at OOPSLA 2025: Compositional Quantum Control Flow with Efficient Compilation in Qunity by Mikhail Mints, Finn Voichick, Leonidas Lampropoulos, and Robert Rand.
The paper Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages by J. Carr, Benjamin Quiring, John Reppy, Olin Shivers, Skye Soss and Byron Zhong will appear at ICFP 2025.
[More …]