Given by ACM SIGPLAN to an institution or individual(s) to recognize the development a software system that has had a significant impact on programming language research, implementations, and tools. The impact may be reflected in the wide-spread 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 email@example.com.
Please use http://awards.sigplan.org/ to submit nominations.
Committee Chair: Michael Hind
Committee Members: Jack Davidson, Jeff Foster, Simon Marlow, Eelco Visser
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.
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.
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.
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
“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.”
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.”