2026 Most Influential POPL Paper Award

Nikhil Swamy (Microsoft), Cătălin Hrițcu (MPI-SP), and co-authors received the 2026 Most Influential POPL Paper Award for their 2016 paper, “Dependent Types and Multi-monadic Effects in F*”.

This award is offered by ACM SIGPLAN every year to the paper deemed most influential from the Principles of Programming Languages (POPL) conference 10 years earlier. POPL is a flagship conference in the area of programming languages and verification, and in 2016 POPL published 59 papers out of 252 submissions.

Citation: “This paper introduced F*, an SMT-aided verification-oriented language that integrates SMT solving (via Z3) with the interactive, proof assistant reasoning of dependent types. By combining Dijkstra monads for weakest-precondition inference with solver automation, F* showed that expressive effectful programs could be verified at scale, shaping the direction of solver-assisted proof-oriented languages. F* became the foundation of Project Everest, and was further developed and maintained by a large team of contributors, enabling applications such as verified cryptographic libraries (e.g., HACL*, EverCrypt), protocols (e.g., miTLS, DY*,  MLS*), and parsers (e.g., EverParse), through the use of DSLs for low-level code (Vale, Low*, Steel, Pulse). The resulting code has been integrated into widely used software stacks, demonstrating real-world impact and validating the paper’s core vision: that SMT automation, tightly integrated with interactive proofs in a principled language design, makes large-scale formal verification practical for high-assurance, high-performance software.”