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.”
Original publication:
Swamy, N., Hrițcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.-Y., Kohlweiss, M., Zinzindohoue, J.-K., Zanella-Bèguelin, S.
Dependent Types and Multi-monadic Effects in F*
https://dl.acm.org/doi/10.1145/2837614.2837655
General note: In case of using gender-assigning attributes we include all those who consider themselves in this gender regardless of their own biological sex.