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 also adjudicate conflicts of interest, appointing substitutes to the committee as necessary.

Recipients of the Influential POPL Paper Award

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

(for 2003) Abstractions from proofs

Citation

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, and VT Rajan, IBM T.J. Watson Research Center

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

Citation

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, University of California, Berkeley

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

Citation

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

Citation

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.

2010: Luca Cardelli and Andrew D. Gordon

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

Citation

"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.

2009: Andrew C. Myers

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

Citation

"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.

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

(for 1998) From System F to Typed Assembly Language

Citation

"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.