Most Influential POPL Paper Award

Presented annually to the author(s) of a paper presented at the POPL held 10 years prior to the award year. The award includes a prize of $1,000 to be split among the authors of the winning paper. The papers are judged by their influence over the past decade.

Selection Committee The award given in year N is for the most influential paper presented at the conference held in year N-10. The selection committee consists of the following members:

  • the current SIGPLAN Chair, ex officio,
  • a member of the SIGPLAN EC appointed as committee Chair by the SIGPLAN Chair,
  • the General Chair and Program Chair for POPL N-10,
  • the General Chair and Program Chair for POPL N-1, and
  • a member of the SIGPLAN EC appointed by the committee Chair.

The SIGPLAN Chair shall adjudicate conflicts of interest, appointing substitutes to the committee as necessary.


2017 Dachuan Yu, Ajay Chander, Nayeem Islam, Igor Serikov

(for 2007): JavaScript Instrumentation for Browser Security


The selected paper presents one of the earliest models of the interaction between the browser and JavaScript. It uses this model to work out the formalization and dynamic enforcement of rich security policies. Since then, people have routinely discovered additional, pernicious security problems based on this model. Eliminating these problems remains an important challenge to this day.

Looking back, the selected paper made a prescient, and influential, contribution to understanding these JavaScript-based security problems. The authors chose a formal, semantic approach to model these problems and potential solutions, while remaining true to the complicated characteristics that make both JavaScript and the browser real-world artifacts.

2016 Xavier Leroy

(for 2006) Formal certification of a compiler back-end or: programming a compiler with a proof assistant


This paper presents the CompCert compiler, a landmark effort in program verification. The paper was (and still is) groundbreaking in that it demonstrates the feasibility of using an interactive theorem prover – specifically, Coq – to both program and formally verify a realistic compiler – specifically, the backend of an optimizing compiler for a significant subset of C. The verification ensures that properties proved about C source code continue to hold of the assembly output of the compiler, thereby filling a major gap in the development of high-assurance software and facilitating a great deal of follow-on work on verified software toolchains. Moreover, CompCert made a convincing case that theorem-proving technology is mature enough to be applied to the full functional verification of realistic systems, and in so doing heralded a new age of “big verification”.

2015 Nate Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, Alan Schmitt

(for 2005) Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View Update Problem


The “view-update problem” is a classic problem in databases: when operating on a partial view of a data structure, how should updates to the view be propagated to the original data structure? This POPL 2005 paper was instrumental in bringing the view-update problem to the attention of the programming languages community and demonstrating the broad relevance of the problem beyond databases. The immediate contributions of the paper were (1) to introduce a general mathematical space of well-behaved bidirectional transformations called “lenses,” and (2) to develop a specific instantiation of this framework in the form of a domain-specific language of combinators for tree transformations, which served as the basis for subsequent tools for editing XML and HTML. More broadly, the paper sparked a great deal of follow-on work in the area of BX (“bidirectional transformations”), leading to a fruitful collaboration between the worlds of databases, programming languages, and software engineering.

2014 Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth McMillan

(for 2004) Abstractions from proofs


Interpolation can be used to construct an inductive invariant for a transition system that is strong enough to prove a given property. Prior to Henzinger et al.’s paper, interpolation had only been applied to model checking of finite-state systems. In this paper, the authors demonstrated a fundamental generalization of Craig interpolation to program analysis by predicate abstraction, opening the door for interpolation to be applied to abstraction refinement of infinite-state systems. This work showed how interpolation offers a fundamental way to explain abstraction refinement in a logical framework and has led to many extensions to increase the power of abstraction in program analysis.

2013 David F. Bacon, Perry Cheng, VT Rajan

(for 2003) A real-time garbage collector with low overhead and consistent utilization


Languages with automatic memory management offer well-known advantages in terms of software engineering, but the use of garbage collection seemed for a long time to place such languages off-limits for hard real-time and embedded systems. Indeed, prior to this highly influential paper, the existing approaches to real-time garbage collection suffered from a number of practical problems: a lack of hard bounds on pause times in the face of fragmentation or large data structures; high space overhead due to the use of copying collection to avoid fragmentation; and uneven mutator utilization due to the use of work-based scheduling algorithms. Bacon, Cheng & Rajan’s paper showed how to overcome all these problems in the design of a real real-time garbage collector for Java. The collector, which was implemented and tested in the Jikes RVM, employed an impressive variety of techniques, such as time-based scheduling and “mostly non-moving” collection, in order to provide guaranteed pause times, consistent mutator utilization, and low space overhead. In short, the paper marked a major advance toward the important goal of turning hard real-time garbage collection into a reality.

2012 George C. Necula, Scott McPeak, and Westley Weimer

(for 2002) CCured: Type-Safe Retrofitting of Legacy Code


This paper showed a path to taking legacy C code and making it safer, by adding type safety guarantees to existing C programs. It uses a combination of static and dynamic techniques to allow programmers to conduct low-level operations while guaranteeing safety properties regarding pointers and minimizing overhead. For many C programs, CCured’s type inference is able to infer that most or all of the pointers are statically verifiable to be type safe. This paper demonstrates the beauty of both dynamic and static types, influencing the design of languages such as C#, and inspiring continuing research on static and dynamic analysis.

2011 Samin Ishtiaq and Peter W. O'Hearn

(for 2001) BI as an Assertion Language for Mutable Data Structures


In applying the logic of bunched implications (BI) to mutable data structures this paper laid the groundwork for the flowering of separation logic (heap models of separation logic are specific BI models), which allows reasoning about programs with dynamically allocated (and deallocated) memory. This paper introduced the ‘frame rule’ which supports local reasoning in separation logic, where specifications and proofs concentrate on just those memory cells manipulated by a program component rather than the entire global program state. Separation logic underlies continuing research on what is described as local reasoning, having diverse application in domains such as program verification and automated parallelization.

2010 Luca Cardelli and Andrew D. Gordon

(for 2000) Anytime, Anywhere: Modal Logics for Mobile Ambients


“Anytime, Anywhere: Modal Logics for Mobile Ambients” by Luca Cardelli and Andrew D. Gordon helped spur a flowering of work in the area of process calculi that continues today. The paper focused on modal logics for reasoning about both temporal and spacial modalities for ambient behaviours, demonstrating techniques that also apply to other process calculi (even those without an explicit notion of location), so contributing to excitement in an area that was growing at that time and continues. The work has led to application of concurrency theory in fields as diverse as security, safety critical applications, query languages for semistructured data, and systems biology.

2009 Andrew C. Myers

(for 1999) JFlow: Practical Mostly-Static Information Flow Control


“JFlow: Practical Mostly-Static Information Flow Control” by Andrew C. Myers demonstrated the practicality of using static information flow analysis to protect privacy and preserve integrity by giving an efficient information flow type checker for an extension of the widely-used Java language. The work has had a significant impact both within and beyond the programming language community. In particular, subsequent work for other languages has largely followed the path laid out in this paper, and the compiler infrastructure developed for JFlow (now called Jif) is widely used as a research platform. Furthermore, using the JFlow work as a basis, several major research initiatives are investigating the challenges of building complex, real-world systems with confidentiality guarantees.

2008 Greg Morrisett, David Walker, Karl Crary, and Neal Glew

(for 1998) From System F to Typed Assembly Language


“From System F to Typed Assembly Language” by Greg Morrisett, David Walker, Karl Crary, and Neal Glew began a major development in the application of type system ideas to low level programming. The paper shows how to compile a high-level, statically typed language into TAL, a typed assembly language defined by the authors. The type system for the assembly language ensures that source-level abstractions like closures and polymorphic functions are enforced at the machine-code level while permitting aggressive, low-level optimizations such as register allocation and instruction scheduling. This infrastructure provides the basis for ensuring the safety of untrusted low-level code artifacts, regardless of their source. A large body of subsequent work has drawn on the ideas in this paper, including work on proof-carrying code and certifying compilers.

2007 George Necula

(for 1997) Proof-carrying Code

2006 Bjarne Steensgaard

(for 1996) Points-to Analysis in Almost Linear Time

2005 Luca Cardelli

(for 1995) A Language with Distributed Scope

2004 Mads Tofte and Jean-Pierre Talpin

(for 1994) Implementation of the Typed Call-by-Value lambda-calculus using a Stack of Regions

2003 Simon Peyton Jones and Philip Wadler

(for 1993) Imperative functional programming