Programming Languages Software Award

Given by ACM SIGPLAN to an institution or individual(s) to recognize the development of a software system that has had a significant impact on programming language research, implementations, and tools. The impact may be reflected in the widespread adoption of the system or its underlying concepts by the wider programming language community either in research projects, in the open-source community, or commercially. The award includes a prize of $2,500. The award is presented at SIGPLAN’s PLDI conference the following June.

All questions about the Programming Languages Software Award should be directed to the SIGPLAN Awards co-Chairs.


Please use to submit nominations. Nominations submitted on or before January 15th will be considered for award that year.

Each nomination should include the following items:

  • Name of the software system being nominated, the name of the institution or team being nominated, and their contact details
  • A short statement explaining why the nominee(s) deserve the award.
  • Name, affiliation, phone number, and email address of each of the developers nominated for the award (the nominees)
  • Name, affiliation, phone number, and email address of the person making the nomination (the nominator).
  • Names and email addresses of 5-10 people who the nominator believes will support the nomination. The awards committee will ask at least three of these people for their opinions.


Award recipients are selected by a committee constituted as follows:

  • The Chair of the committee shall be a member of the SIGPLAN Executive Committee (EC), and shall be appointed by the executive committee.
  • The SIGPLAN EC Chair shall be an ex-officio member of the committee. If the SIGPLAN EC Chair is unable to serve, he or she may appoint another member of the SIGPLAN EC as a substitute.
  • The steering committees of the major SIGPLAN Conferences, POPL, PLDI, ICFP, and SPLASH, shall each appoint a member to the committee.

The current committee comprises:

Conflicts of Interest

If any member of the committee has a conflict of interest with a given nominee they shall declare that to the committee; once so declared, conflicts of interest shall not automatically prevent a committee member from taking part in the selection process. However, if a member of the committee, or the chair of the committee, feels that the association of a committee member with a nominee would interfere with impartial consideration of the nominees, that conflicted member shall be absented from the relevant parts of the discussion. If a committee member has conflicts of interest with more than one nominee, the Chair of the Committee may ask the constituency that appointed the committee member to select a replacement member. The SIGPLAN EC Chair will adjudicate as necessary


2023 OCaml


The OCaml Compiler Distribution is the reference implementation of the OCaml language, a dialect of ML that aims to be pragmatic, both in language features and implementation, encouraging a simple programming style that yields good performance and usability. It has a large user base in industry, research, and education throughout the world, and was used to implement a number of other impactful systems, notably in verification: Coq proof assistant, CompCert verified compiler, Why3 verified programming environment, Frama-C, Astrée and Gillian static analyzers, Infer, Hack and Flow projects at Meta, SLAM/SDV and F* at Microsoft, etc.

The nominated contributors are:

  • David Allsopp, Tarides
  • Florian Angeletti, INRIA
  • Stephen Dolan, Jane Street
  • Damien Doligez, INRIA
  • Alain Fritsch, Lexifi
  • Jacques Garrigue, Nagoya University
  • Xavier Leroy, Collège de France
  • Anil Madhavapeddy, Cambridge University
  • Luc Maranget, INRIA
  • Nicolás Ojeda Bär, Lexifi
  • Gabriel Scherer, INRIA
  • KC Sivaramakrishnan, Tarides
  • Jérôme Vouillon, CNRS
  • Leo White, Jane Street

Selection Commitee: Antony Hosking, Dominique Devriese, Manu Sridharan, Andreas Rossberg, David Grove

2022 CompCert


CompCert is a fully verified compiler for C that is actually usable on real source code and that produces decent target code on real-world architectures. It seeded a new age of formal verification by dispelling the myth that formal methods could only be done on toy programs in the lab. As a shared artifact it has enabled the software systems verification community to work together, in the same way that GCC or LLVM has done in earlier generations, putting real-world C programs on a solid formal foundation. It currently targets PowerPC, ARM, RISC-V, and x86, supporting all of ISO C99 except unstructured switch statements, longjmp, and variable-length array types. CompCert is today available under commercial and noncommercial open-source licenses, and used in the real world for security-critical control software for emergency power generators and for flight control and navigation algorithms, by companies including Airbus France. It remains an important shared infrastructure for ongoing research.

The nominated contributors are:

  • Xavier Leroy
  • Sandrine Blazy
  • Zaynah Dargaye
  • Jacques-Henri Jourdan
  • Michael Schmidt
  • Bernhard Schommer
  • Jean-Baptiste Tristan

Selection Commitee: Antony Hosking, Dominique Devriese, Manu Sridharan, Andreas Rossberg, David Grove

2021 WebAssembly


WebAssembly is the first new broadly-adopted language in web browsers since JavaScript. It is the fruit of a genuine collaboration between all major browser vendors, backed by an unprecedented effort to place the new language on a sound formal footing. WebAssembly’s formalization effort both shows the benefits of bringing PL techniques to widely-adopted languages—the disparate browser implementations all worked correctly with no deviation from the specification—and makes WebAssembly fertile ground for future research on web languages. Despite only being around for a short time, WebAssembly has already served as the base for multiple distinguished paper efforts from both industry and academia. Initially created as a supplement to the Web stack, it also has seen quick adoption in other domains that share similar requirements, such as mobile and edge computing, IoT, confidential computing, blockchain and smart contract platforms. On the Web, it has enabled many large-scale applications.

The nominated contributors are:

  • Andreas Rossberg
  • Derek Schuff
  • Bradley Nelson
  • JF Bastien
  • Ben L. Titzer

2020 Pin


Pin is a dynamic binary instrumentation platform, developed and actively supported for over 15 years by Intel. Through an extensive API for instrumentation of applications at different abstraction levels, Pin supports the creation of custom program analysis and profiling tools, hardware simulators, or binary translators. By supporting such scenarios for complex production applications, Pin has enabled research across many domains including programming languages, computer architecture, security, mobile systems, networking, embedded systems, operating systems, and high-performance computing. In particular, Pin opened the door for instrumentation of x86 binaries across a wide range of platforms and operating systems, thus changing the landscape of computer architecture and programming language research. To maintain transparency towards applications while achieving unprecedented low runtime overheads, Pin uses a wide array of optimizations rooted in the dynamic binary translation and instrumentation technology pioneered by the SIGPLAN community, such as just in time compilation of basic blocks, and trampolines from such code fragments to others. Pin is also widely used in the classroom of numerous universities at both undergraduate and graduate levels.

The nominated contributors are:

  • Artur Klauser
  • Greg Lueck
  • Mark Charney
  • Gail Lyons
  • Geoff Lowney
  • Aamer Jaleel
  • Harish Patil
  • Vijay Janapa Reddi
  • Kim Hazelwood
  • S. Bharadwaj Yadavalli
  • Ramesh Peri
  • Elena Demikhovsky
  • Ady Tal
  • Moshe Bach
  • Alex Skaletsky
  • CK Luk
  • Steven Wallace
  • Tevi Devor
  • Robert Muth
  • Nadav Chachmon

2019 Scala


Scala is one of the few programming languages from academia that has had a significant impact on the world as well as on programming languages research. It enjoys significant industrial adoption, with early adopters like Twitter and LinkedIn serving as catalysts; it forms the basis of the widely used Apache Spark data analytics platform. Scala’s impact on PL research includes the idiom of implicits, which have found their way into other languages; attempts to formalize Scala’s type system have pushed the boundaries of type systems research, culminating in the Dependent Object Types (DOT) calculus. In addition, Scala has been a fertile research ground for m etaprogramming, macros, staging, and embedded domain-specific languages, including DSLs for machine learning and GPU execution (Delite and OptiML).

The nominated contributors are:

  • Martin Odersky
  • Adriaan Moors
  • Aleksandar Prokopec
  • Heather Miller
  • Iulian Dragos
  • Nada Amin
  • Philipp Haller
  • Sébastien Doeraene
  • Tiark Rompf

2018 Racket


Racket comprises a programming language, an IDE, and a large ecosystem of libraries and packages. Its contributions have been singularly significant both in research and education. Over the past 20 years, Racket has enabled a wide spectrum of programming language research: it initiated work on recursive, first-class modules, provided a test bed for functional reactive programming, generalized software contracts to higher-order settings, and participated in launching the area of gradual typing. Most importantly, Racket is a leading programming language for making programming languages, due to is results on language extensibility, an active area of research for the emerging language community. With DrRacket, the Racket community has innovated the design of pedagogic IDEs, introducing the transparent read-eval-print loop, algebraic stepping, and the idea of hierarchies of teaching languages. The IDE has played a key role in spreading the word about novel text books on programming (“How to Design Programs”) and programming languages (“Programming Languages: Implementations and Applications” and “Semantics Engineering”), bringing concepts dear to SIGPLAN to students all over the world.

The nominated contributors are:

  • Eli Barzilay
  • Matthias Felleisen
  • Robert Bruce Findler
  • Matthew Flatt
  • Shriram Krishnamurthi
  • Jay McCarthy
  • Sam Tobin-Hochstadt

2016 V8 JavaScript Engine


V8 is an open-source JavaScript engine developed at Google that revolutionized the use of JavaScript, firmly establishing it as a platform both in the browser and on the server. V8’s success is in large part due to the efficient machine code it generates; because JavaScript is a highly dynamic object-oriented language, many experts believed that this level of performance could not be achieved. V8, whose principal architect is Lars Bak, relies on more than 20 years of research in compilation and implementation techniques initially developed for Beta, Self, and Sun’s Hotspot JVM. These techniques include hidden class recovery in a classless language (based on profiled executions of the JS programs) followed by on-the-fly in-place inline caching. V8’s garbage collector is also very high quality, important for (e.g.,) graphically intensive interactive web apps. V8’s techniques have influenced other major JS engines, contributing to the JavaScript-as-a-platform revolution. Its performance breakthrough has had a major impact on the adoption of JavaScript, which is nowadays used on the browser, the server, and probably tomorrow on the small devices of the internet-of-things.

2015 Z3 Theorem Prover


Z3 has changed the way SIGPLAN members tackle problems of static analysis and program synthesis. Such problems, which form a significant part of programming languages research and development, had long been tackled using various automated decision procedures. But in the 2000s, Z3 enabled qualitative and quantitative leaps, in both the difficulty and the size of problems that could be solved. Today, Z3 is a standard tool, not only because of its inherent qualities, such as heuristics that militate in favor of short proofs and short refutations, but because its developers have continually improved it through close engagement with their users. Such users include many researchers in program analysis and synthesis, and improvements made on behalf of one user often help many others working in the same domain. In the domain of decision procedures that support program analysis and synthesis, after many years of accumulated improvements, Z3 is now the unquestioned leader.

2014 The GNU Compiler Collection (GCC)


The GNU Compiler Collection (GCC) provides a portable, production-quality, standards-compliant, highly optimizing compiler, supporting more architectures, programming languages, and operating environments than any other comparable tool. It provides the toolchain that underpins all of the GNU/Linux distributions, popular websites, and embedded environments.

GCC provides the foundation for numerous experiments in programming language design, including the early C++ language, numerous evolutions of the C and C++ standards, parallel programming with OpenMP, and the Go programming language. GCC has been used by many research projects, leading to high-impact publications and contributions to the development trunk, including sophisticated instruction selection based on declarative machine descriptions, auto-tuning techniques, transactional memory, and polyhedral loop nest optimizations.

GCC is the product of hundreds of person-years of work over its 27 years of existence. This award recognizes the GCC developer community for the substantial impact it has had on the programming language community and the larger software industry.

2013 The Coq proof assistant


The Coq proof assistant provides a rich environment for interactive development of machine-checked formal reasoning. Coq is having a profound impact on research on programming languages and systems, making it possible to extend foundational approaches to unprecedented levels of scale and confidence, and transfer them to realistic programming languages and tools. It has been widely adopted as a research tool by the programming language research community, as evidenced by the many papers at SIGPLAN conferences whose results have been developed and/or verified in Coq. It has also rapidly become one of the leading tools of choice for teaching the foundations of programming languages, with courses offered by many leading universities and a growing number of books emerging to support them. Last but not least, these successes have helped to spark a wave of widespread interest in dependent type theory, the richly expressive core logic on which Coq is based.

As a software system, Coq has been in continuous development for over 20 years, a truly impressive feat of sustained, research-driven engineering. The Coq team continues to develop the system, bringing significant improvements in expressiveness and usability with each new release.

In short, Coq is playing an essential role in our transition to a new era of formal assurance in mathematics, semantics, and program verification.

2012 Jikes Research Virtual Machine (RVM)


The SIGPLAN Software Award for 2012 goes to the Jikes Research Virtual Machine (RVM), an open-source virtual computer implemented in the Java programming language, and capable of running programs written in Java and many other languages that compile to JVM bytecodes. The award nomination names 32 contributors to the Jikes RVM project, but the project actually has more than double that number of contributors. Jikes RVM was the first Java-in-Java virtual machine and contains many innovations, especially on adaptive optimization and memory management.

The high quality and modular design of Jikes has made it easy for researchers to develop, share, and compare advances in programming language implementation. The Jikes RVM core team has nurtured and supported a large community of researchers; this is witnessed by more than 200 papers, at least 40 dissertations, close to 25 courses, and research at almost 100 universities, that are based on the Jikes RVM.

The nominated contributors are:

  • Bowen Alpern
  • Matthew Arnold
  • Clement Attanasio
  • John Barton
  • Steve Blackburn
  • Maria Butrico
  • Perry Cheng
  • Tony Cocchi
  • Julian Dolby
  • Peter Donald
  • Steven Fink
  • Daniel Frampton
  • Robin Garner
  • David Grove
  • Michael Hind
  • Derek Lieber
  • Kathryn McKinley
  • Mark Mergen
  • Eliot Moss
  • Ton Ngo
  • Igor Peshansky
  • Filip Pizlo
  • Feng Qian
  • Ian Rogers
  • Vivek Sarkar
  • Mauricio Serrano
  • Janice Shepherd
  • Stephen Smith
  • Peter F. Sweeney
  • Martin Trapp
  • Kris Venstermans
  • John Whaley

2011 Simon Peyton Jones and Simon Marlow for the Glasgow Haskell compiler

The cash prize is being donated to


Simon Peyton Jones and Simon Marlow receive the SIGPLAN Software Award as the authors of the Glasgow Haskell Compiler (GHC), which is the preeminent lazy functional programming system for industry, teaching, and research. GHC has not only provided a language implementation, but also established the whole paradigm of lazy functional programming and formed the foundation of a large and enthusiastic user community. GHC’s flexibility has supported experimental research on programming language design in areas as diverse as monads, generalized algebraic data types, rank-N polymorphism, and software transactional memory. Indeed, a large share of the research on lazy functional programming in the last 5-10 years has been carried out with GHC. Simultaneously, GHC’s reliability and efficiency has encouraged commercial adoption, in the financial sector in institutions like Credit Suisse and Standard Chartered Bank, and for high assurance software in companies like Amgen, Eaton, and Galois.

A measure of GHC’s influence is the way that many of the ideas of purely functional, “typeful programming” have been carried into newer languages and language features. including C#, F#, Java Generics, LINQ, Perl 6, Python, and Visual Basic 9.0. Peyton Jones and Marlow have been visionary in the way that they have transitioned research into practice. They have been role models and leaders in creating the large and diverse Haskell community, and have made GHC an industrial-strength platform for commercial development as well as for research.

2010 Chris Lattner for the LLVM Compiler Infrastructure


Chris Lattner receives the SIGPLAN Software Award as the author of the LLVM Compiler Infrastructure, which has had a dramatic impact on our field. LLVM is being used extensively in both products and research, for traditional and non-traditional compiler problems, and for a diverse set of languages. LLVM has had a significant influence on academic research, not just in compilers but also in other areas, such as FPGA design tool. Many researchers cite the “elegance of LLVM’s design” as one of the reasons for using LLVM. LLVM has also had an impact on industrial projects and products; it is used at major companies including Apple and Google. For example, LLVM is an integral part of Apple’s software stack in Mac OS X. Furthermore, as with academic research, LLVM is finding its way into unexpected applications of compiler technology. In summary, LLVM has had an incredible impact on both industry and academia and its elegance has enabled it to be used for a wide range of applications.”