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 http://awards.sigplan.org/ to submit nominations. Nominations submitted on or before January 15th will be considered for award that year.
Each nomination should include the following items:
Award recipients are selected by a committee constituted as follows:
The current committee comprises:
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
Citation:
Rust is the first industrial strength programming language to offer a compelling answer to the challenge of being a safe systems programming language: one with fine-grained control over low-level resources while avoiding the security vulnerabilities of unsafe languages. It provides: control over low-level resources via a C-style programming model, with a minimal runtime and avoiding garbage collection for predictable performance; and safety via a type system that systematically eliminates out-of-bounds accesses, use-after-free bugs, and data races. Rust achieves this by embodying innovations from academic PL research—linear/affine types, ownership types, traits—combined with usable standard libraries. Born out of many years of research and experimentation, Rust tackles the real-world challenges and issues needed for practical adoption. Rust has been recognized as one of a handful of Safer Languages by NIST, and is increasingly deployed in industry for its safety benefits by large and small companies alike.
The nominated contributors are:
- Aaron Turon
- Alex Crichton
- Brian Anderson
- Dave Herman
- Felix S. Klock II
- Graydon Hoare
- Marijn Haverbeke
- Nicholas D. Matsakis
- Patrick Walton
- Tim Chevalier
- Yehuda Katz
- All Rust Contributors Past and Present
Selection Commitee: Antony Hosking, Dominique Devriese, Manu Sridharan, Andreas Rossberg, David Grove
Citation:
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
Citation:
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
Citation:
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
Citation:
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
Citation:
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
Citation:
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
Citation:
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.
Citation:
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.
Citation:
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.
Citation:
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.
Citation:
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
The cash prize is being donated to haskell.org
Citation:
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.
Citation:
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.”