## Programming Languages Achievement Award

Given by ACM SIGPLAN to recognize an individual or individuals who has made a significant and lasting contribution to the field of programming languages. The contribution can be a single event or a life-time of achievement. The award includes a prize of $5,000. The award is presented at SIGPLAN's PLDI conference the following June.

**Nominations**

Please use http://awards.sigplan.org/ to submit nominations.

## Recipients of the Achievement Award

## 2014: Neil Jones

Neil Jones is a pioneer of programming-language methods. He introduced control-flow analysis for higher-order programs, binding-time analysis to tame self-applicable partial evaluation, what is known today as "Jones optimality", and size-change termination analysis. Neil is also noted for bridges he established between programming languages and complexity/computability theory, e.g., characterizing Turing's Universal Machine as self interpretation, Kleene's S-m-n theorem as partial evaluation, Kleene's second recursion theorem as reflection, and the expressive power of typed cons-free functional languages by means of complexity classes. His pioneering work on complexity theory included the development of completeness for P and solving the spectrum problem (the basis of finite model theory). Lastly, Neil is a tireless and inspiring mentor, and he has written several influential textbooks that are testaments to his thesis that programs are data objects and that programming languages are a cornerstone of computer science.

## 2013: Patrick and Radhia Cousot

Patrick and Radhia Cousot are the co-inventors of abstract interpretation, a unifying theory of sound abstraction and approximation of structures involved in various domains of computer science, such as formal semantics, specification, proof, and verification. In particular, abstract interpretation has had a major impact on the development of the static analysis of software. In their original work, the Cousots showed how to relate a static analysis to a language's standard semantics by means of a second, abstract semantics that makes precise which features of the full language are being modeled and which are being discarded (or abstracted), providing for the first time both a formal definition of and clear methodology for designing and proving the correctness of static analyses. Subsequently, the Cousots contributed many of the building blocks of abstract interpretation in use today, including chaotic iteration, widening, narrowing, combinations of abstractions, and a number of widely used abstract domains. This work has developed a remarkable set of intellectual tools and has found its way into practice in the form of widely used libraries and frameworks. Finally, the Cousots and their collaborators have contributed to demonstrating the utility of static analysis to society. They led the development of the AstrÈe static analyzer, which is used in the medical, automotive, and aerospace industry for verifying the absence of a large class of common programming errors in low-level embedded systems code. This achievement stands as one of the most substantial successes of program verification to date.

## 2012: Matthias Felleisen

The SIGPLAN 2012 Achievement award has been won by Matthias Felleisen, an exemplary researcher whose work covers theory, practice, and education, with each reinforcing the others. He has made fundamental contributions across the entire spectrum of the programming language field. He introduced evaluation contexts as a notation for specifying operational semantics, and progress-and-preservation proofs of type safety, both of which are used in scores of research papers each year, often without citation. His other contributions include small-step operational semantics for control and state, A-normal form, delimited continuations, mixin classes and mixin modules, a fully-abstract semantics for Sequential PCF, web programming techniques, higher-order contracts with blame, and static typing for dynamic languages.

## 2011: Sir Charles Antony Richard Hoare, FRS, FREng, FBCS

Citation"Tony Hoare's long career in computing is studded with seminal engineering and scientific contributions to Programming Languages; his views on programming language design have been recognized as profound even by those who declined to follow his advice.

Two contributions stand out as fundamental: the development of what is now known as Hoare logic, and Communicating Sequential Processes. Hoare logic is a system for reasoning about imperative programs. It was introduced in the 1969 article "An Axiomatic Basic for Computer Programming", which is perhaps the most influential 6-page paper ever published in CACM. Drawing on earlier work of Robert Floyd, an entire sub-area of computer science has developed from Hoare's initial ideas; many modern verification systems build on Hoare logic.

Only 9 years later, CACM published Hoare's paper on Communicating Sequential Processes (CSP). Contemporary with Milner's CCS, but pursuing complementary goals, CSP has been enormously influential. It provided the basis for the occam programming language and its realization in the Transputer; it has been used for modeling and verifying the concurrency properties of critical software systems; and it inspired a flowering of subsequent concurrency research.

Although either of these contributions would alone justify the achievement award, Hoare is doing more with his Unifying Theories research, which aims to unify theories of programming across paradigm, abstraction level and semantic style. Beyond all of this, Tony is renowned for his unfailing courtesy, his inspiration, and his dedication to his chosen calling. He is the epitome of a scholar and a gentleman."

## 2010: Gordon D. Plotkin

Citation"Professor Gordon D. Plotkin has made fundamental advances in almost every area of the theory of programming languages. His contributions have helped to establish the mathematical foundations on which the scientific study of programming languages are based. His 1975 paper "Call-by-name, Call-by-value, and the λ-calculus" exposed the relationship between the reduction semantics of the λ-calculus and its operational semantics, as defined by Landin's SECD machine.

## 2009: Rod Burstall

Citation"Professor Rod Burstall has made deep, seminal contributions to the design of programming languages and the field of program verification.

## 2008: Barbara Liskov

Citation"Professor Barbara Liskov has had tremendous impact on the fields of programming languages, operating systems, distributed systems, and information security. Much of her early research focus was on data abstraction, modularity, and encapsulation as typified by the CLU programming language.

## Past Recipients of the Achievement Award

2007: Niklaus Wirth

2006: Ron Cytron, Jeanne Ferrante, Barry Rosen, Mark Wegman, and Kenneth Zadeck

2005: Erich Gamma, Richard Helm, Ralph Johnson, John Vlissides

2004: John Backus

2003: John Reynolds

2002: John McCarthy

2001: Robin Milner

2000: Susan Graham

1999: Ken Kennedy

1998: Fran Allen

1997: Guy Steele