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.
All questions about the Programming Languages Achievement Award should be directed to email@example.com.
Please use http://awards.sigplan.org/ to submit nominations.
Luca Cardelli has made exceptional contributions to the field of programming languages. He has a remarkable ability to re-invent himself every decade or so and yet continue to make true innovations. His contributions span many areas: software; language design, including experimental languages; programming language foundations; and the interaction of programming languages and biology.
He is a leading language designer. He was one of the designers of Modula-3, which played a major role in popularising the notion of type-safe programming, and was a key influence on Java and C#. Thus, his work helped lay the foundations for today’s near-universal industrial acceptance of type-safe programming languages. He also designed several important experimental languages, including Obliq, a distributed higher-order scripting language, and Polyphonic C#, a distributed extension of C#. He implemented the first compiler for ML.
He is a leading and hugely influential computer scientist. His most sustained research activity has been in establishing the semantic and type-theoretic foundations of programming languages. Two of his most prominent works are his 1985 paper “On understanding types, data abstraction, and polymorphism” (with Wegner) and his 1996 book “A Theory of Objects” (with Abadi). Other important works of his concern the semantics of multiple inheritance in object-oriented languages and explicit substitutions in the lambda-calculus.
More recently, he has focused on modeling global and mobile computation, via the Ambient Calculus and spatial logics. His work pioneered an influential way of describing, programming, and reasoning about global and mobile computation, in terms of formal calculi and language constructs. It also connected with an important line of work on semi-structured data, and led, indirectly, to his current interest in biology and stochastic systems.
In both his own work and his great scientific influence Cardelli has made lasting contributions to the field of programming languages.
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.
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.
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.
Matthias tests his ideas by building real systems, working in the framework of PLT Scheme, later renamed Racket, which includes interactive development environments, interactive debugging and flow analysis, documentation tools, and support for language levels and multiple languages. He has coauthored a series of influential texts, including four ‘little’ books—The Little Schemer, The Seasoned Schemer, A Little Java, and The Little MLer—the widely used textbook How to Design Programs, and a monograph on Semantics Engineering. He founded a series of workshops and projects to support K–12 teaching, including TeachScheme!, Reach Java, and Program by Design. Moreover, he has nurtured a new generation of researchers, who are now respected in their own right and pursue the same goals of excellence, rigor, and real-world impact that have characterized Matthias’s work.
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.
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. In the process, he defined what it meant for a calculus and a semantics to correspond: this launched the study of operational semantics as it is now understood. He invented Structural Operational Semantics as a technique for specifying the semantics of a wide range of programming languages, concurrent as well as sequential; this form of semantics is now one of the basic working tools of researchers developing new programming languages and type systems.
Plotkin’s contributions to the development of the mathematical theory of domains, and its applications to the denotational semantics of programming languages, have been of fundamental importance: they include his powerdomain construction, systematic development of the general theory of the solution of recursive domain equations, and his work on PCF and the full abstraction problem.
Plotkin’s work with Glynn Winskel on event structures is the basis for reasoning about distributed systems, process algebras, and reactive systems. Event structures have been enormously influential in the development of models of concurrency. He has also investigated the logical foundations of computer security, including logics for specifying authorization policies for computer systems. Plotkin continues to make bold and deep contributions, for example, in his current work on the algebraic theory of effects, and on languages and calculi for biochemical modelling. Taken together, Gordon Plotkin’s contributions over the past four decades exhibit a range and depth unmatched in the field.
Professor Rod Burstall has made deep, seminal contributions to the design of programming languages and the field of program verification. These contributions, which many of us now take for granted, include the introduction of algebraic datatypes coupled with pattern-matching clausal function definitions as found in Hope, ML, Haskell and Coq; the generalization and use of structural induction for proving properties of programs; the fold-unfold method for deriving efficient, provably-correct programs from easy to understand prototypes; mechanisms for reasoning about pointer-based, imperative programs that directly led to the development of separation logic; proof techniques and connections to modal logic for reasoning about concurrent programs; and the use of dependent types and algebraic specifications for constructing module systems that directly influenced SML and OCaml. Through these amazing contributions and his collaborations and mentorship, he helped build one of the most important centers of programming research at Edinburgh, which was eventually institutionalized as the Laboratory for Foundations of Computer Science.”
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. At the time, CLU incorporated a number of advanced features, such as modular encapsulation of abstract data types, bounded polymorphism, exceptions, and iterator abstraction that had clear influence over successive languages including Ada, Modula-3, C++, and Java. Through CLU, the related books and articles, her work on behavioral subtyping, and her courses on programming methodology, Professor Liskov changed the way that a generation of engineers thought about and constructed large software systems. Professor Liskov’s work on the Argus project also brought to the fore the idea of integrating transactions and orthogonal persistence into a programming language with an aim towards building reliable distributed systems. More recently, her work on information flow control helped to start a research focus on end-to-end security using language-based mechanisms for enforcement.”