The Robin Milner Young Researcher Award is given by ACM SIGPLAN to recognize outstanding contributions by young investigators in the area of programming languages. Individuals are eligible if their computer-related professional career (graduate school or full-time employment, whichever began first) started no earlier than 20 years prior to the nomination deadline. At the discretion of the award committee, eligibility may be adjusted to account for documented career interruptions, including (but not limited to) family leave, medical leave, or military service. Questions of eligibility should be directed to the award committee chair in advance of nomination (see below).
The award includes a prize of $2,500.
All questions about the Robin Milner Young Researcher Award should be directed to the SIGPLAN Awards co-Chairs.
Robin Milner (13 January, 1934 - 20 March, 2010)
Robin Milner was, for decades, a leading light in programming language research, developing many of the ideas that now form the backbone of the field. Among Milner’s biggest gifts to the field was his passion for mentoring and nurturing young colleagues, many of whom have grown into world leaders in their own right. It seems fitting that an award be established in his name to further encourage new generations of outstanding researchers.
Milner’s academic career began with posts at City University (University of London), Swansea, and Stanford. In 1973 he joined the University of Edinburgh, where in 1986 he co-founded the legendary Laboratory for Foundations of Computer Science (LFCS). In 1995 he left Edinburgh for Cambridge, where he was head of the Computer Laboratory for several years. He became a Fellow of the Royal Society in 1998 and received the Turing Award in 1991. The Turing Award citation includes this capsule summary of his contributions:
Working in challenging areas of computer science for twenty years, Robin Milner has the distinction of establishing an international reputation for three distinct and complete achievements, each of which has had and will continue to have a marked, important, and widespread effect on both the theory and practice of computer science:
LCF, the mechanization of Scott’s Logic of Computable Functions, probably the first theoretically based yet practical tool for machine-assisted proof construction. ML, the first language to include polymorphic type inference together with a type-safe exception-handling mechanism. CCS, a general theory of concurrency. In addition, he formulated and strongly advanced full abstraction, the study of the relationship between operational and denotational semantics.
A key ingredient in all of his work was to combine deep insight into mathematical foundations of the subject with an equally deep view of the key engineering issues, thus allowing the feedback of theory into practice in an exciting way. Further, his style of scholarship, rigor, and attention to aesthetic quality sets a high example for all to follow.
Nominations can be submitted at any time using the Web form at https://awards.sigplan.org. Nominations submitted on or before January 15th will be considered for award that year. The committee may decline to make an award in a given year if there are no suitable nominees.
Award recipients are selected by a committee constituted as follows:
The current committee is:
Because this award is intended to recognize persons of major influence, it is likely that several members of the committee may have worked with, or co-authored articles with, the nominees, and may have a conflict of interest. The primary mechanism for handling such conflicts will be to declare them 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:
Nate Foster is a world leader in programming languages and software-defined networking. His skills as a PL researcher run the gamut: adept at design, theory, implementation, and applications, a combination rare to find in a single individual. His work brings elegant PL techniques to bear on fundamental problems in networking, makes pioneering contributions to both fields, and enables verification approaches for networking implementations. Notably, this is the second field Nate has opened up: his PhD work introduced “lenses” as a language construct for bidirectional tree transformations applied to the database view update problem. His work has been recognized with multiple distinguished paper and “test of time” awards. Nate also gives significant service & leadership to the PL community on conference program and steering committees, mentoring workshops, and representative to influential working groups.
- Selection committee: Antony Hosking, Sandrine Blazy, Suresh Jagannathan, Ranjit Jhala, Éric Tanter.
Citation:
Viktor has become a world leader in semantics and verification research. His body of work includes fundamental and influential contributions to the study of concurrency, in particular separation logic and relaxed memory models. His landmark doctoral thesis developed RGSep, the first extension of concurrent separation logic to support formal proofs about fine-grained concurrent algorithms. His work on Cave presented the first fully automatic verifier for establishing linearizability of a class of concurrent data structures, including ones with non-fixed linearization points. His work on CompCertTSO presented the first verified compiler for a concurrent language under a relaxed memory model. He developed the first direct (and mechanized) proof of soundness for concurrent separation logic (CSL) based on operational semantics—beautifully simple compared to prior proofs and a key enabler for proving soundness of more advanced program logics like CAP and Iris. He developed the first separation logic for the C/C++ relaxed memory model—a tour-de-force achievement compared to the standard CSL which assumes sequential consistency. This spawned a whole body of work on modular verification of concurrent data structures under relaxed memory models. His work has found and corrected a number of serious flaws in the C/C++ concurrency model, which led to changes in the C++ standard. And his “promising” semantics for relaxed-memory concurrency offered one of the first viable solutions to the 30-year-old “out-of-thin-air” problem and spawned much follow-on work. His work on GenMC presented the first efficient model checkers for relaxed-memory C/C++ programs with optimality guarantees about their state space exploration. Recent work together with his postdoc Azalea Raad (now faculty at Imperial), presented the first “persistency semantics” for non-volatile memory on multicore architectures. Viktor is not only highly-cited and incredibly prolific—he is also a true pioneer, repeatedly exploring dauntingly technical problems in the semantics and verification of concurrent programs before others dare to try.
- Selection committee: Antony Hosking, Sandrine Blazy, Suresh Jagannathan, Ranjit Jhala, Éric Tanter.
Citation:
Emina Torlak is a leader in the area of automated verification. She has made both conceptual contributions and built tools that are state of the art and widely used. On the conceptual side, the notion of a solver-aided programming language is hers and has quickly become standard terminology. Torlak defined a set of linguistic abstractions that elegantly generalized various prior point solutions that integrated solvers into languages. The rapidity with which the notion of solver-aided languages took hold indicates both how natural the idea is in retrospect and how relevant it is to a large group of researchers in the PL community.
Torlak demonstrated that it was feasible to build a fairly general-purpose solver-aided language with Rosette. The idea of a lightweight symbolic VM is principled and effective. She and her colleagues have successfully deployed Rosette in a wide and impressive variety of applications across domains, notably in systems. Further, Rosette is seeing broad application, including by researchers outside of the PL community. Finally, Torlak’s tool Kodkod for finding solutions to Alloy models from her dissertation work has been and continues to be widely used.
In summary, Emina Torlak has contributed an impressive breadth of fundamental insights. Just as impressive is her depth of contribution to open-source software that others have been able to build their research on.
- Selection committee: Emery Berger, Michelle Strout, Michael Hicks, Eijiro Sumii, Todd Millstein.
Citation:
Eran Yahav has a record of sustained, high-impact contributions to the programming languages research community over nearly two decades. Much of his work has concerned effective static reasoning about concurrent programs, which is a longstanding challenge due to the complex and non-local ways in which threads can interact with one another. Yahav developed novel abstractions for verifying safety and correctness properties of concurrent programs and used them to validate non-trivial concurrent algorithms in Java. Later, he extended and applied program synthesis techniques to concurrent programs in creative ways, for example, demonstrating how to synthesize a correct concurrent version of a sequential algorithm and how to automatically repair an existing concurrent algorithm through additional synchronization. Most recently, Yahav has been an early leader in the area of “big code,” leveraging machine learning techniques to solve difficult programming tasks, including code search, code completion, and reverse engineering. This work has influenced others in the research community to pursue this research direction and has led to practical software engineering tools for programmers.
- Selection committee: Emery Berger, Michelle Strout, Derek Dreyer, Eijiro Sumii, Todd Millstein.
Citation:
Martin Vechev is a prolific researcher who has made major contributions to many areas of programming languages. He is a pioneer who is often one of the first in the PL community to move into a new area. He is particularly well known for his seminal papers and tools at the interface of programming languages and machine learning. An example tool is JSNice, which deobfuscates JavaScript code by learning a probabilistic graphical model from a large corpus of programs, which is then used to predict improved variable names and perform statistical type inference. Another example at this interface is his work on using abstract interpretation for proving safety properties of deep neural networks, such as robustness. His many other contributions include significant advances in concurrent memory management, synthesis of synchronization code for concurrent programs, and efficient program analysis.
Citation:
Ranjit Jhala has demonstrated a long track-record of producing foundational and impactful contributions to our understanding of programming language theory and implementation. Jhala was one of the principal developers of the BLAST automatic verification tool for checking temporal safety properties of C programs. A key contribution was the notion of lazy abstraction which integrates three phases of the software model checking loop: abstraction, checking and refinement. Jhala developed an algorithm for model checking safety properties that continuously builds and refines a single abstract model on demand by the model checker. This allows different parts of the model to exhibit just the degrees of freedom required to verify a desired property. The work on lazy abstraction has proved to be very influential in the verification community. Jhala also used Craig interpolation to efficiently construct, from a given abstract error trace that cannot be concretized, a parsimonious abstraction that removes the trace. He developed the method for programs with arithmetic and pointer expressions, and call-by-value function calls. This resulting technique was successfully applied to programs over 130,000 lines which was previously not possible.
Jhala has significantly advanced the practical application of refinement types which allow programmers to attach additional specifications to existing types. These additional specifications allow interesting properties to be proved about code, such as invariants over recursively defined data structures. The problem with such specifications is that they can be too onerous to write down and get right. Jhala’s work on Liquid Types showed that a useful and expressive class of these specifications can be inferred in a largely automatic way, making the approach far more practical at a reasonable cost. Jhala’s work with Liquid Types has significantly extended the state-of-the-art, adding a notion of predictability and decidability often not found in SMT-based software verification, and extending the usability and expressiveness of formal type systems.
Jhala has also worked on data race detection, information flow and timing analysis for Javascript and code analytics. Jhala has also written a lengthy tutorial on Liquid Haskell, proved to be an excellent communicator and mentor who has given many engaging and inspiring presentations, and served extensively on program committees of top conferences.
- Selection committee: Antony Hosking, Chandra Krintz, Xavier Leroy, François Pottier and Satnam Singh.
Citation:
Derek Dreyer has made deep, creative research contributions of great breadth. His areas of impact are as diverse as module systems, data abstraction in higher-order languages, mechanized proof systems and techniques, and concurrency models and semantics. He has refactored and generalized the complex module systems of SML and OCaml; devised logical relations and techniques that enabled advances in reasoning about higher-order imperative programs; and developed novel separation logics for modular verification of low-level concurrent programs. His research papers are a model of clarity and depth, and he has worked actively to translate his foundational ideas into practice – most recently with the RustBelt project to provide formal foundations for the Rust language. Additionally, Dreyer has contributed leadership, support, and mentorship in activities such as the PLMW series of workshops, which are instrumental in growing the next generation of PL researchers.
- Selection committee: Kathleen Fisher, Antony Hosking, Chandra Krintz, Xavier Leroy, Yannis Smaragdakis.
Citation:
Stephanie Weirich has made deep and sustained contributions to programming language research in the areas of functional programming, dependent types, and proof assistants. She has been one of the main investigators of type inference for Generalized Algebraic Data Types (GADTs), and, with collaborators at Microsoft Research, she helped put this technology into practice in the widely used GHC Haskell implementation. Weirich, with collaborators at Penn and Cambridge, also initiated and led the POPLMark challenge, a highly visible and influential effort to promote the use of proof assistants for formalizing and checking the theory of programming languages. She has also greatly contributed to the understanding of dependent types in practical programming languages, and is now involved in an effort to bring the benefits of dependent types to Haskell. Finally, Weirich has made substantial contributions to the programming languages community, notably with her involvement in the Programming Languages Mentoring Workshop (PLMW), which has blossomed into a highly successful workshop that is held several times a year at venues including POPL, PLDI, ICFP, and SPLASH; Weirich was one of the original organizers of PLMW at POPL 2012, and continues to serve on the workshop’s steering committee.
- Selection committee: Tom Ball, Matthew Flatt, Antony Hosking, Sorin Lerner, Yannis Smaragdakis.
Citation:
David Walker has made deep and varied contributions to programming language research, but always with an eye towards emerging and surprising applications of foundational theory. He was one of the co-authors of the work on Typed Assembly Language (TAL), which showed how conventional type systems could be brought to bear on low-level machine code, and which forms the basis for today’s typed virtual machines such as Microsoft’s .NET. Focusing on the need for better reasoning principles for pointers, he helped develop Alias Types, the Calculus of Capabilities, and region-based formalisms that influenced the design of type systems for modern languages like Cyclone, Vault, and Rust. Walker also provided semantic foundations for secure program monitoring, and used his insights to develop new tools for enforcing security policies on legacy code. Long before “big data” was a hot topic, he and his co-authors designed languages for processing large, ad-hoc data collections. Recognizing trends in hardware, he developed new techniques for verifying the safety of programs executing on faulty processors. And, most recently, foreseeing the rise of software-defined networking, he has worked with people from both the networking and PL communities to develop new, high-level languages (Frenetic, Pyretic) for programming networks. In summary, Prof. Walker is a groundbreaking researcher in programming languages, connecting foundations to novel applications.
Citation:
Sumit Gulwani has made pioneering contributions to the field of programming languages, especially in the areas of program analysis and program synthesis. Building on his foundational work in program analysis including using randomized algorithms, improving abstract interpretation, and reasoning about programs as continuous functions, Dr. Gulwani recognized the important connection between program verification and program synthesis. His research has demonstrated that imprecise human intent, in the form of examples, natural language, and other kinds of input, can be transformed into incomplete program specifications, which together with ranking techniques can then be used to synthesize intended programs, empowering users to accomplish complex and repetitive programming tasks without needing any knowledge of programming. His contributions include algorithms for synthesizing string transformation programs by examples, published in POPL 2011, and the technical basis for “Flash Fill”, a new feature shipping in Microsoft’s Excel 2013. He has since then extended this line of algorithmic work to synthesizing programs in several other important domains and also broadly advertised this line of work by publishing in top-tier ACM conferences in various other areas including AI, machine learning, HCI, databases, and knowledge discovery. He has also championed the application of program synthesis techniques to developing intelligent tutoring systems for numerous subject domains including introductory programming, mathematics, logic, and automata theory. The visionary aspects of his work were recently recognized by the CACM Editorial Board when two of his recent papers appeared as CACM Research Highlights in the same issue, and a summary of his work on computer-aided Education was accepted to appear as a CACM article.
In summary, Dr. Gulwani is a highly motivated, creative, and inter-disciplinary researcher whose vision is to empower computer users around the world to be more productive and educated. His insights in using program synthesis to address problems in end-user programming and education will have deep and lasting influence.
Citation:
Lars Birkedal is a world leader in foundational programming languages research, and the pre-eminent researcher of his generation in the area of programming language semantics. His work, spanning a multitude of top journal and conference publications, has had significant impact in many areas. These include foundational type theory, compiler implementation, Milner’s bigraphical reactive systems, logics and models for relational parametricity, and verification technology for semantically complex languages.
Birkedal is a pioneer in “bringing semantics into the 21st century”: developing rigorous and scalable semantic and verification techniques to account for the needs and complexities of modern languages. Toward this end in particular, he has (a) made numerous advances to the theory and practice of region-based memory management, (b) made fundamental contributions to the theory of relational parametricity, which underlies our semantic understanding of abstract data types, and (c) developed higher-order separation logics and other powerful tools for the modular verification of realistic imperative, object-oriented, and concurrent programming patterns.
In short, Birkedal has tackled hard problems of paramount importance to the future of programming language research, and has made startling advancements across the board. He has done so both independently, via the research group he built up at the IT University of Copenhagen, and also through fruitful collaborations with an impressive network of international colleagues, thus setting an excellent example for other junior researchers.
Citation:
The SIGPLAN 2012 Robin Milner Young Researcher Award goes to Shriram Krishnamurthi, a prolific researcher who brings programming language theory to bear in many other disciplines, thus exposing its foundational value. His research contributions range from type soundness proofs for Java and influential extensions thereof, through foundational aspects of web programming, to model-driven development and empirical studies. The most important aspects of Krishnamurthi’s research are
- that it cuts across multiple disciplines, including education, software engineering, formal methods and security, but always building on the firm ground of programming language theory;
- its orientation towards practicality and applicability to standard platforms: programming systems for teaching, reactive web programming, executable JavaScript semantics, and analysis techniques for security policies;
- that it has resulted not only in publications, but also in practical systems that are used in academia and industry; and
- the clarity of its exposition and presentation.
- Shriram is also an influential educator, reaching out beyond the university to infect school kids with algebraic thinking.
In summary, Shriram is an extraordinarily broad researcher, making sustained contributions in important and exciting areas, with a commitment to education that is ensuring that his ideas have even broader impact.