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
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.
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.
One paper co-authored by PLUM members will appear at TOPLAS 2025: Modal Crash Types for WAR-Aware Intermittent Computing by Myra Dotzel, Farzaneh Derakhshan, Milijana Surbatovich, and Limin Jia.
The paper Webs and Flow-Directed Well-Typedness Preserving Program Transformations by Benjamin Quiring and David Van Horn together with John Reppy and Olin Shivers will appear at PLDI 2025.
One paper co-authored by PLUM members will appear at POPL 2025: Pantograph: A Fluid and Typed Structure Editor by Jacob Prinz, Henry Blanchette, and Leonidas Lampropoulos.
Nikhil Kamath won second place at the presented his research on Seedzer: A Full-Stack Pipeline for Fuzzing Deep Learning Compilers at the 2024 ICFP Student Research Competition!
[More …]