Diese Auszeichnung wird jährlich von der ACM SIGPLAN für die einflussreichste Arbeit der letzten zehn Jahre auf der Konferenz "Principles of Programming Languages" (POPL) verliehen. Die POPL ist eine der führenden Konferenzen im Bereich Programmiersprachen und Verifikation. Im Jahr 2016 wurden von den 252 eingereichten Beiträgen 59 auf der POPL veröffentlicht.
Zitation: "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."
Originale Publikation:
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
Allgemeiner Hinweis: Mit einer möglichen Nennung von geschlechtszuweisenden Attributen implizieren wir alle, die sich diesem Geschlecht zugehörig fühlen, unabhängig vom biologischen Geschlecht.
