Most Influential ICFP Paper Award

Presented annually to the author(s) of a paper presented at the ICFP 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. This award was initiated in 2007 (for 1997).

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 ICFP N-10,
  • the General Chair and Program Chair for ICFP 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 ICFP Paper Award

2013: Didier Le Botlan and Didier Rémy

For 2003 ML^F: Raising ML to the Power of System F


Le Botlan and Rémy's paper on MLF presented a major technical breakthrough in type inference for first-class polymorphism. Remarkably, by going from ML to a system that is more expressive than System F, principal types could be recovered. The paper was the first and only paper (to date) to present a type inference and unification algorithm with all the "good" features of ordinary ML inference and unification, except on a richer universe of types and constraints that allowed impredicative instantiation. The MLF system enjoys most general unifiers, completeness properties, and robustness under program transformations, with user type annotations providing the oracles needed to reach the expressiveness of System F and beyond. The MLF paper has been highly influential on subsequent work in type inference for first-class polymorphism, and is a must-read for anyone interested in the topic.

2012: Robert Findler and Matthias Felleisen

For 2002 Contracts for higher-order functions


Assertion-based contracts have proven very useful for dynamically enforcing first-order program invariants in procedural languages, but until 2002 they had not been supported in languages with higher-order functions. Findler and Felleisen's paper filled this gap, presenting "the first assertion-based contract checker for languages with higher-order functions." The paper also spawned a great deal of follow-on work on such topics as the semantics of blame assignment and the integration of static typing and dynamic contract checking. Higher-order contracts have become a central component of the Racket (formerly PLT Scheme) system -- one of the major software artifacts of the functional-programming community -- which serves as both a research testbed and an effective tool for programming-language education.

2011: Claudio Russo

For 2001 Recursive Structures for Standard ML


Various attempts at extending ML modules with recursions were made starting in the early 90's. However, they all ran into a nasty typing issue later dubbed the "double-vision problem" by Derek Dreyer. Russo's ICFP 2001 paper was the first to propose a correct and practical solution to this problem. The solution played very cleverly on the nonstandard formalization of ML modules developed in his thesis. Building on this novel insight, the ICFP 2001 paper develops a complete design for recursive modules in ML, which Russo implemented in Moscow ML and which is complete enough to handle many desirable examples. Russo's design was the main source of inspiration for adding recursive modules in OCaml, taking recursive modules from an open research issue to a realised language feature that simply works.

2010: Koen Claessen and John Hughes

(for 2000) Quickcheck: a lightweight tool for random testing of Haskell programs


This paper presented a very simple but powerful system for testing Haskell programs that has had significant impact on the practice of debugging programs in Haskell. The paper describes a clever way to use type classes and monads to automatically generate random test data.

2009: Malcolm Wallace and Colin Runciman

(for 1999) Haskell and XML: Generic combinators or type-based translation?,


Malcolm Wallace and Colin Runciman's 1999 ICFP paper "Haskell and XML: Generic combinators or type-based translation?" was one of the first papers to spell out the close connection between functional programming languages and XML. It described a typed correspondence between XML's document type definitions (DTD) and Haskell datatypes.

2008: Lennart Augustsson

(for 1998) Cayenne — a language with dependent types,


Lennart Augustsson's 1998 ICFP Paper “Cayenne: A language with dependent types” made dependently-typed programming accessible to non-type theorists. The language design was a bold one, both in its use of dependent types and in its adoption of an undecidable type system. Although the idea seemed quite radical at the time, it allowed future work to break out of the straight-jacket of decidable type systems.

2007: Conal Elliott and Paul Hudak

(for 1997) Functional Reactive Animation,


"Functional Reactive Animation" by Conal Elliott and Paul Hudak was the first published paper on functional reactive programming. It described a collection of data types and functions that comprised an embedded domain-specific language called Fran for composing interactive, multi-media animations. The key abstractions were first-class behaviors and events.

2006: Julia L. Lawall and Harry G. Mairson

(for 1996) Optimality and inefficiency: what isn't a cost model of the lambda calculus?


Julia Lawall and Harry Mairson's 1996 ICFP paper "Optimality and inefficiency: What isn't a cost model of the lambda calculus?" exposed a fundamental problem with proposed algorithms for optimal reduction. Starting with Jean-Jacques Lévy's seminal work in 1978, the goal of optimal reduction was to correctly normalize lambda-calculus terms without duplicating redexes.