2020’s edition of the Symposium on the Principles of Programming Languages (POPL) anchored an exciting and inspiring week filled with technical talks and discussions among its 600 participants. People from around the world came to New Orleans to be a part of the event. For the first time the conference was carbon neutral, thanks to Microsoft which purchased carbon offsets for all attendees’ travel (and POPL’s main tracks were live streamed for those who couldn’t make it). This year’s edition also witnessed a wide variety of community-building and mentoring events.
This post provides an overview of this 47th edition of POPL, from both a technical and non-technical perspective. Links to papers, slides, and recorded videos of the talks are available at the POPL 2020 website, which also has lots of information about the event.
What is POPL about?
POPL is one of the oldest computer science conferences, and has published many seminal papers. Its purview is the theoretical foundations of programming languages, and over the years its particular focus has broadened and shifted. This year, of the 247 papers submitted for review, the top three author-designated topics were Types (77 papers), Language Design (70 papers), and Functional Languages (69 papers) — in total these three topics covered 87 percent of all submissions. The next three most popular topics were Program Analysis (61 papers), Semantic Models (47 papers), and Program Logics (45 papers).
A committee of 53 scientists reviewed these submissions over two rounds to decide which to publish in PACMPL’s POPL issue, and to invite for presentation at the event. POPL employed the Toronto Paper Matching System (TPMS) to partially automate the process of assigning papers to reviewers. The review process employed a form of double blinding: A paper’s authors were hidden from a reviewer while they initially evaluated the paper, but revealed to them after their written review was submitted (the rationale for which is discussed somewhat in Hicks’ POPL’12 Chair’s report). Short responses from authors to their paper’s reviews were taken into account prior to initial decisions, which were made during a multi-day, on-line PC meeting. After a subsequent round of review and revision, 68 papers were accepted, 36 of which had a successfully evaluated artifact. A six-person sub-committee of the PC selected six Distinguished Papers from the final list (all linked below).
Considering these papers and the event itself, we might wonder: what is the POPL community working on today? There is a huge variety of topics, but there are also some core themes. Looking at the event as a whole, we can see two such themes: (1) Formal verification and reasoning, often for the purpose of ensuring security, and (2) Machine learning and probabilistic programming. Even so, there was a cornucopia of work outside these themes.
Formal Verification and Reasoning (Often for Security)
Over the years, POPL and its collocated events have focused on methods to formally reason about program properties, especially including security. With software flaws being at the root of high-profile events like Heartbleed and the Equifax data breach, researchers are developing new mathematics and methods to establish that software does what it should.
Cristina Cifuentes gave the second day’s keynote talk, What is a Secure Programming Language? focusing on how the language can help programmers avoid some of the common pitfalls leading to security holes. The Workshop on Principles of Secure Compilation (PriSC) and the Workshop on High Assurance Systems Engineering (HASE) both looked at mechanisms and methods justifying increased trust in software systems. Several technical papers at POPL developed new logics and type systems for ensuring that software has desired security properties, or proved that interventions like sandboxing or constant-time compilation get the job done.
The colocated conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) considered a variety of approaches for analyzing programs. The Conference on Certified Proofs and Programs (CPP) — which had a record number of submissions this year — focused on techniques for mechanizing proofs of program properties, while the Workshop on Automated Deduction for Separation Logics (ADSL) and CoqPL (Workshop on Coq for Programming Languages) considered particular logics and frameworks for doing so. Researchers also offered tutorials on verified quantum computing (to go along with the new Programming Languages for Quantum Computing workshop), reasoning about programs, and mechanizing semantic properties.
To cap off CPP, the POPLMark 15 Year Retrospective panel contemplated the impact of the POPLmark challenge, first laid down in 2005, on research in mechanizing proof, and what direction that work might take in the future. Proof assistants — the tools for mechanizing proofs — also played an important role in several papers and verification tools, e.g., there were several new papers on program logics based on the Iris framework and one of the Distinguished Papers presented Interaction Trees, a formal model for representing first-order effectful recursive programs in the Coq proof assistant.
Machine Learning and Probabilistic Programming
Researchers are aggressively exploring how machine learning techniques can be used to solve problems across many sub-areas of computer science. While machine learning can be used for programming tasks often tackled in PL research, a theme of this year’s POPL was the reverse: PL can help ML, too.
Martin Vechev, this year’s ACM SIGPLAN Robin Milner Young Researcher Award winner, argued in his keynote talk Can Programming Languages Research impact Deep Learning 2.0? that traditional PL topic areas such as abstract interpretation and optimization can be used to solve important open problems in deep learning. Several papers at POPL considered programming language support for automatic differentiation of functions, a key feature of machine learning algorithms. One paper focused on first-order programs and the challenges associated with conditionals and loops whereas another focused on higher-order functions and the connections to linearity, to ensure efficiency of backpropagation. There was also a Distinguished Paper on how to use new models derived from work on the differential lambda calculus to prove fundamental results for lambda calculi, relying on Taylor expansion for approximation.
Hongseok Yang’s keynote provided an introduction to probabilistic programming languages (as did a tutorial on the topic a few days before). These can be used to express models to which to apply Bayesian inference, which is a key method in modern machine learning. He explained how ideas from program analysis may improve probabilistic programming systems. A deeper technical dive on the topic was provided at the colocated Workshop on Languages for Inference (Lafi), and several POPL papers considered probabilistic programming. This year, POPL had three sessions on probabilistic programming and new results were presented on many topics, including higher-order probabilistic programming; probabilistic programming and quantum computing; and probabilistic separation logics (which were used to prove security properties, as indicated above).
Cornucopia
Aside from these two themes, there were many other interesting topics. The PEPM and PADL collocated events focused on partial evaluation and declarative languages, respectively. Program synthesis continued to grab some spotlight: there was a tutorial on it to start the week; there were five technical papers presented during the week; and at the end of the week we learned that the paper From Program Verification to Program Synthesis (by Saurabh Srivastava, Sumit Gulwani, and Jeff Foster) won POPL’s Most Influential Paper award (having been published at POPL’10, ten years before).
Types were explored in several ways, e.g., in connection with concurrency, where types were used both to tame concurrent programming through novel so-called label-dependent session types, and to increase our understanding of the fundamental connection between proofs and processes through a novel type system for concurrent functional programming based on multiplicative linear logic. New results on type inference were also presented, including novel undecidability results for type inference for the dependent object type calculus (a Distinguished Paper) which underlies the Scala programming language, and kind inference for data types (also a Distinguished Paper). There were also new results on dependent types, e.g., an investigation of how to combine dependent types and effects, and how to implement dependent type systems using macros. There were two papers with foundational results on gradual typing, and a colocated workshop on the topic.
Language design spanned widely and included papers on a new alias model for the Rust programming language called Stacked Borrows; a formal semantics for the POSIX shell; and new techniques for memory management of nested-parallel programs used to run on multicore machines.
Within the area of functional languages, one of the Distinguished Papers presented new results on so-called semi+naive evaluation for a higher-order version of datalog. New methods for cost analysis of functional programs were also presented, both by extracting recurrences from the programs and by analysis using Liquid Haskell.
In the area of program analysis new results included a novel polynomial time algorithm for dynamic race detection and a reachability analysis for reducing the simulation time of distributed network routing protocols. One of the Distinguished Papers presented new results on almost linear-time verification of a class of while programs using a new kind of Kleene algebras called guarded Kleene algebras with tests.
Mentoring and Community Building
POPL is not just about technical ideas, it’s also about building community. Of the 496 POPL attendees, 250 were students. POPL provided extra encouragement to students in various ways, including through the ACM student research competition, and well-established and highly successful Programming Languages Mentoring Workshop (PLMW), whose talks were recorded for the first time.
This year introduced a number of additional mentoring events. In particular, the mentoring breakfasts for students, post-docs, junior researchers and academics were highly successful and inspiring, with over 150 participants attending over three days. For the first time, POPL featured W@POP which specifically aimed to connect women PL faculty, post-docs and students and to provide a low-pressure atmosphere to foster building one’s support group. POPL also featured an LGBTQ Lunch whose goal was to allow queer researchers in PL to connect with each other and to foster an atmosphere within the PL community that welcomes, supports, and values researchers of all identities. In addition, POPL hosted an Ally Skill Workshop which taught simple everyday ways for allies to use their privilege and influence to support people who are targets of systemic oppression in their workplaces and communities.
POPL was also proud to help launch the newly formed SIGPLAN CARES Committee (Committee to Aid REporting on discrimination and haraSsment policy violations). The role of CARES is to serve as a resource consisting of well-known and respected people in the programming languages community who are approachable and willing to listen to and help people who experience discrimination and harassment at our events (more information see SIGPLAN Cares website).
Thanks!
With its fantastic technical content and myriad opportunities for making new friends and collaborators, we look back on POPL 20 as a great success. We, the organizers, would like to thank all the authors of submitted papers, the program committee, past POPL PC Chairs and the POPL Steering Committee for advice, Laurent Charlin for TPMS, Eddie Kohler for HotCRP, Azadeh Farzan for handling PC chair conflicts, all 885 (!) users of https://popl20.hotcrp.com for papers and reviews, and the rest of the organizing committee. See you next year in Copenhagen, Denmark!
Bios: Lars Birkedal was the Program Chair of POPL 2020. He is a Professor of Computer Science at Aarhus University, a Fellow of the ACM, an elected member of the Royal Danish Academy of Sciences and Letters, and the winner of the ACM SIGPLAN Milner Award in 2013. Michael Hicks is the current Steering Committee Chair of POPL. He is a Professor of Computer Science at the University of Maryland, the past SIGPLAN Chair (2015-2018), and the editor of this blog. Brigitte Pientka was the General Chair of POPL 2020. She is an Associate Professor in the School of Computer Science at McGill University, Montreal, Canada, and serves on the editorial boards of the Journal of Functional Programming and the ACM Transactions on Computational Logic, and is an executive editor of the Logical Methods in Computer Science.
Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.
