Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.

The symposium is sponsored by ACM SIGPLAN, in cooperation with ACM SIGACT and ACM SIGLOG.

Dates
Tracks
You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 16 Jan

Displayed time zone: Belfast change

09:00 - 10:05
Welcome & Keynote IResearch Papers at Sala I + II
Chair(s): Peter O'Hearn Facebook
09:00
5m
Day opening
Welcome
Research Papers
Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU), Stephanie Weirich University of Pennsylvania, USA
Media Attached
09:05
60m
Talk
Automated Fault-Finding and Fixing at Facebook
Research Papers
Mark Harman Facebook and University College London
Media Attached
10:35 - 12:03
Reasoning about Probabilistic ProgramsResearch Papers at Sala I
Chair(s): Jan Hoffmann Carnegie Mellon University
10:35
22m
Talk
Formal Verification of Higher-Order Probabilistic Programs
Research Papers
Tetsuya Sato University at Buffalo, SUNY, USA, Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Justin Hsu University of Wisconsin-Madison, USA
Link to publication DOI Media Attached File Attached
10:57
22m
Talk
A Separation Logic for Concurrent Randomized Programs
Research Papers
Joseph Tassarotti Carnegie Mellon University, Robert Harper
Link to publication DOI Media Attached File Attached
11:19
22m
Talk
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Research Papers
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen University
Link to publication DOI Media Attached File Attached
11:41
22m
Talk
Trace Abstraction Modulo Probability
Research Papers
Calvin Smith University of Wisconsin - Madison, Justin Hsu University of Wisconsin-Madison, USA, Aws Albarghouthi University of Wisconsin-Madison
Link to publication DOI Media Attached
10:35 - 12:03
ConcurrencyResearch Papers at Sala II
Chair(s): Ori Lahav Tel Aviv University
10:35
22m
Talk
A True Positives Theorem for a Static Race Detector
Research Papers
Nikos Gorogiannis , Peter W. O'Hearn Facebook and University College London, Ilya Sergey Yale-NUS College and National University of Singapore
Link to publication DOI Pre-print Media Attached File Attached
10:57
22m
Talk
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Research Papers
Roland Meyer , Sebastian Wolff TU Braunschweig
Link to publication DOI Pre-print Media Attached File Attached
11:19
22m
Talk
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Research Papers
Klaus v. Gleissenthall University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Alexander Bakst , Deian Stefan University of California San Diego, Ranjit Jhala University of California, San Diego
Link to publication DOI Media Attached
11:41
22m
Talk
Weak-Consistency Specification via Visibility Relaxation
Research Papers
Michael Emmi SRI International, Constantin Enea Université Paris Diderot
Link to publication DOI Media Attached File Attached
12:03 - 13:45
Wednesday LunchResearch Papers at Lunch Room
12:03
1h42m
Lunch
Lunch
Research Papers

13:45 - 14:51
Probabilistic Programming and SemanticsResearch Papers at Sala I
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
13:45
22m
Talk
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic
Research Papers
Maria I. Gorinova The University of Edinburgh, Andrew D. Gordon Microsoft Research and University of Edinburgh, Charles Sutton University of Edinburgh
Link to publication DOI Pre-print Media Attached File Attached
14:07
22m
Talk
A Domain Theory for Statistical Probabilistic ProgrammingDistinguished Paper
Research Papers
Matthijs Vákár University of Oxford, Ohad Kammar University of Edinburgh, Sam Staton University of Oxford
Link to publication DOI Pre-print Media Attached File Attached
14:29
22m
Talk
Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Research Papers
Feras Saad Massachusetts Institute of Technology, Marco Cusumano-Towner MIT-CSAIL, Ulrich Schaechtle Massachusetts Institute of Technology, USA, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka MIT
Link to publication DOI Media Attached File Attached
13:45 - 14:51
CategoriesResearch Papers at Sala II
Chair(s): Nicolas Tabareau Inria
13:45
22m
Talk
Familial Monads and Structural Operational Semantics
Research Papers
Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry
Link to publication DOI Media Attached File Attached
14:07
22m
Talk
Bindings as Bounded Natural Functors
Research Papers
Jasmin Blanchette Vrije Universiteit Amsterdam, Lorenzo Gheri Middlesex University London, Andrei Popescu Middlesex University, London, Dmitriy Traytel ETH Zurich
Link to publication DOI Media Attached File Attached
14:29
22m
Talk
Categorical Combinatorics of Scheduling and Synchronization in Game Semantics
Research Papers
Paul-André Melliès CNRS and University Paris Diderot
Link to publication DOI Media Attached File Attached
15:21 - 16:27
Machine Learning and Linear AlgebraResearch Papers at Sala I
Chair(s): Aws Albarghouthi University of Wisconsin-Madison
15:21
22m
Talk
code2vec: Learning Distributed Representations of Code
Research Papers
Uri Alon Technion, Meital Zilberstein Technion, Omer Levy University of Washington, USA, Eran Yahav Technion
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
An Abstract Domain for Certifying Neural Networks
Research Papers
Link to publication DOI Media Attached
16:05
22m
Talk
Closed Forms for Numerical Loops
Research Papers
Zachary Kincaid Princeton University, Jason Breck University of Wisconsin - Madison, John Cyphert University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
Link to publication DOI Media Attached File Attached
15:21 - 16:27
Capabilities and Session Types IResearch Papers at Sala II
Chair(s): Dominic Orchard University of Kent, UK
15:21
22m
Talk
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Research Papers
Lau Skorstengaard Aarhus University, Dominique Devriese Vrije Universiteit Brussel, Belgium, Lars Birkedal Aarhus University
Link to publication DOI Media Attached File Attached
15:43
22m
Talk
Two sides of the same coin: Session Types and Game Semantics
Research Papers
Simon Castellan Imperial College London, UK, Nobuko Yoshida Imperial College London
Link to publication DOI Pre-print Media Attached File Attached
16:05
22m
Talk
Exceptional Asynchronous Session Types: Session Types without Tiers
Research Papers
Simon Fowler The University of Edinburgh, Sam Lindley University of Edinburgh, UK, J. Garrett Morris University of Kansas, USA, Sara Décova
Link to publication DOI Pre-print Media Attached File Attached
16:37 - 17:43
Quantum ProgrammingResearch Papers at Sala I
Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)
16:37
22m
Talk
Quantitative Robustness Analysis of Quantum Programs
Research Papers
Shih-Han Hung University of Maryland, Kesha Hietala University of Maryland, Shaopeng Zhu University of Maryland, Mingsheng Ying University of Technology Sydney, Michael Hicks University of Maryland, College Park, Xiaodi Wu University of Oregon, USA
Link to publication DOI Media Attached
16:59
22m
Talk
Game Semantics for Quantum Programming
Research Papers
Pierre Clairambault CNRS & ENS Lyon, Marc De Visme ENS Lyon, Glynn Winskel
Link to publication DOI Media Attached
17:21
22m
Talk
Quantum Relational Hoare Logic
Research Papers
Dominique Unruh University of Tartu
Link to publication DOI Pre-print Media Attached File Attached
16:37 - 17:43
Session Types IIResearch Papers at Sala II
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
16:37
22m
Talk
Interconnectability of Session-Based Logical ProcessesTOPLAS
Research Papers
Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London
Link to publication DOI Pre-print Media Attached
16:59
22m
Talk
Distributed Programming using Role-Parametric Session Types in Go
Research Papers
David Castro-Perez Imperial College London, Raymond Hu Imperial College London, Sung-Shik Jongmans Open University of the Netherlands, Nicholas Ng Imperial College London, Nobuko Yoshida Imperial College London
Link to publication DOI Pre-print Media Attached File Attached
17:21
22m
Talk
Less is More: Multiparty Session Types Revisited
Research Papers
Alceste Scalas Imperial College London, Nobuko Yoshida Imperial College London
Link to publication DOI Pre-print Media Attached File Attached
18:00 - 18:30
Wednesday Evening Program IResearch Papers at Sala I
18:00
30m
Talk
Microsoft Research: Engage, Verify, Open
Research Papers
Thomas Ball Microsoft Research
Media Attached
18:30 - 19:30
Wednesday Evening Program IIStudent Research Competition at Galeria
18:30
60m
Social Event
Student Research Competition and Reception supported by Microsoft Research
Student Research Competition

Thu 17 Jan

Displayed time zone: Belfast change

09:00 - 10:06
Type Abstraction and EffectsResearch Papers at Sala I
Chair(s): Benjamin Delaware Purdue University
09:00
22m
Talk
Abstraction-Safe Effect Handlers via Tunneling
Research Papers
Yizhou Zhang Cornell University, Andrew Myers Cornell University
Link to publication DOI Media Attached
09:22
22m
Talk
Abstracting Algebraic Effects
Research Papers
Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław
Link to publication DOI Media Attached
09:44
22m
Talk
Fully Abstract Module Compilation
Research Papers
Karl Crary Carnegie Mellon University
Link to publication DOI Media Attached File Attached
09:00 - 10:06
SynthesisResearch Papers at Sala II
Chair(s): Robbert Krebbers Delft University of Technology
09:00
22m
Talk
Structuring the Synthesis of Heap-Manipulating ProgramsDistinguished Paper
Research Papers
Nadia Polikarpova University of California, San Diego, Ilya Sergey Yale-NUS College and National University of Singapore
Link to publication DOI Pre-print Media Attached File Attached
09:22
22m
Talk
FrAngel: Component-Based Synthesis with Control Structures
Research Papers
Kensen Shi Stanford University, Jacob Steinhardt Stanford University, Percy Liang Stanford University
Link to publication DOI Pre-print Media Attached File Attached
09:44
22m
Talk
Hamsaz: Replication Coordination Analysis and Synthesis
Research Papers
Farzin Houshmand University of California, Riverside, Mohsen Lesani University of California, Riverside
Link to publication DOI Media Attached
10:30 - 12:30
Finalist Poster PresentationsStudent Research Competition at Sala III
10:36 - 12:04
Gradual TypesResearch Papers at Sala I
Chair(s): Nikhil Swamy Microsoft Research
10:36
22m
Talk
Type-Driven Gradual Security with ReferencesTOPLAS
Research Papers
Matías Toro University of Chile, Ronald Garcia University of British Columbia, Éric Tanter University of Chile & Inria Paris
DOI Media Attached File Attached
10:58
22m
Talk
Gradual Type Theory
Research Papers
Max S. New Northeastern University, Daniel R. Licata Wesleyan University, Amal Ahmed Northeastern University, USA
Link to publication DOI Media Attached File Attached
11:20
22m
Talk
Gradual Parametricity, RevisitedDistinguished Paper
Research Papers
Matías Toro University of Chile, Elizabeth Labrada University of Chile, Éric Tanter University of Chile & Inria Paris
Link to publication DOI Pre-print Media Attached File Attached
11:42
22m
Talk
Live Functional Programming with Typed Holes
Research Papers
Cyrus Omar University of Chicago, Ian Voysey Carnegie Mellon University, Ravi Chugh University of Chicago, Matthew Hammer None
Link to publication DOI Pre-print Media Attached File Attached
10:36 - 12:04
Separation Logic and Memory SemanticsResearch Papers at Sala II
Chair(s): Ilya Sergey Yale-NUS College and National University of Singapore
10:36
22m
Talk
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Research Papers
Aleš Bizjak Aarhus University, Daniel Gratzer , Robbert Krebbers Delft University of Technology, Lars Birkedal Aarhus University
Link to publication DOI Media Attached File Attached
10:58
22m
Talk
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
Research Papers
José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Gabriela Sampaio Imperial College London, UK, Philippa Gardner Imperial College London
Link to publication DOI Media Attached File Attached
11:20
22m
Talk
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Research Papers
Alasdair Armstrong University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Alastair Reid Arm Ltd, Kathryn E. Gray University of Cambridge, Robert M. Norton University of Cambridge, Prashanth Mundkur SRI International, Mark Wassell University of Cambridge, Jon French University of Cambridge, Christopher Pulte University of Cambridge, Shaked Flur University of Cambridge, Ian Stark The University of Edinburgh, Neel Krishnaswami Computer Laboratory, University of Cambridge, Peter Sewell University of Cambridge
Link to publication DOI Media Attached File Attached
11:42
22m
Talk
Exploring C Semantics and Pointer Provenance
Research Papers
Kayvan Memarian University of Cambridge, Victor B. F. Gomes University of Cambridge, UK, Brooks Davis SRI International, Stephen Kell University of Kent, Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge, Peter Sewell University of Cambridge
Link to publication DOI Media Attached File Attached
12:04 - 13:45
Thursday LunchResearch Papers at Lunch Room
12:04
1h41m
Lunch
Lunch
Research Papers

13:45 - 14:51
Type Inference IResearch Papers at Sala I
Chair(s): Michael Hicks University of Maryland, College Park
13:45
22m
Talk
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Research Papers
Jana Dunfield Queen's University, Kingston, Ontario, Neel Krishnaswami Computer Laboratory, University of Cambridge
Link to publication DOI Media Attached
14:07
22m
Talk
Abstracting Extensible Data Types; Or, Rows By Any Other Name
Research Papers
J. Garrett Morris University of Kansas, USA, James McKinna
Link to publication DOI Media Attached
14:29
22m
Talk
Polymorphic Symmetric Multiple Dispatch with Variance
Research Papers
Gyunghee Park KAIST, Oracle Labs, Jaemin Hong KAIST, South Korea, Guy L. Steele Jr. Oracle Labs, Sukyoung Ryu KAIST, South Korea
Link to publication DOI Media Attached File Attached
13:45 - 14:51
Weak MemoryResearch Papers at Sala II
Chair(s): Scott Owens University of Kent, UK
13:45
22m
Talk
On Library Correctness under Weak Memory Consistency
Research Papers
Azalea Raad MPI-SWS, Germany, Marko Doko MPI-SWS, Germany, Lovro Rožić MPI-SWS, Germany, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Pre-print Media Attached File Attached
14:07
22m
Talk
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models
Research Papers
Anton Podkopaev Higher School of Economics, JetBrains Research, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Pre-print Media Attached File Attached
14:29
22m
Talk
Grounding Thin-Air Reads with Event Structures
Research Papers
Soham Chakraborty Max Planck Institute for Software Systems, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Media Attached File Attached
15:21 - 16:49
Type Inference IIResearch Papers at Sala I
Chair(s): Niki Vazou IMDEA Software Institute
15:21
22m
Talk
Dynamic Type Inference for Gradual Hindley–Milner Typing
Research Papers
Yusuke Miyazaki Kyoto University, Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
Gradual Typing: A New Perspective
Research Papers
Giuseppe Castagna CNRS - Université Paris Diderot, France, Victor Lanvin IRIF, Université Paris Diderot, France, Tommaso Petrucciani DIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. Siek Indiana University, USA
Link to publication DOI Media Attached File Attached
16:05
22m
Talk
Intersection Types and Runtime Errors in the Pi-Calculus
Research Papers
Ugo Dal Lago University of Bologna, Italy / Inria, France, Marc De Visme ENS Lyon, Damiano Mazza CNRS, Akira Yoshimizu INRIA
Link to publication DOI Media Attached File Attached
16:27
22m
Talk
Principality and Approximation under Dimensional Bound
Research Papers
Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
Link to publication DOI Media Attached File Attached
15:21 - 16:49
TimeResearch Papers at Sala II
Chair(s): Andrew Myers Cornell University
15:21
22m
Talk
Type-Guided Worst-Case Input Generation
Research Papers
Di Wang Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Research Papers
Conrad Watt University of Cambridge, John Renner University of California, San Diego, Natalie Popescu University of California San Diego, Sunjay Cauligi UCSD, Deian Stefan University of California San Diego
Link to publication DOI Media Attached File Attached
16:05
22m
Talk
Modular Quantitative Monitoring
Research Papers
Rajeev Alur University of Pennsylvania, Konstantinos Mamouras University of Pennsylvania, Caleb Stanford University of Pennsylvania
Link to publication DOI Media Attached File Attached
16:27
22m
Talk
CSS Minification via Constraint SolvingTOPLAS
Research Papers
Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Chih-Duo Hong University of Oxford
Media Attached File Attached
17:00 - 18:00
Business MeetingResearch Papers at Sala I + II
17:00
15m
Other
PC Chair Report
Research Papers
Stephanie Weirich University of Pennsylvania, USA
Media Attached
17:15
10m
Awards
SIGPLAN Awards
Research Papers
Benjamin C. Pierce University of Pennsylvania
Media Attached
17:25
5m
Other
POPL 2020 Announcement
Research Papers
Brigitte Pientka McGill University, Lars Birkedal Aarhus University
Media Attached
17:30
10m
Other
NSF funding for PL
Research Papers
Rance Cleaveland University of Maryland
Media Attached
17:40
10m
Other
SIGPLAN Climate Committee Report
Research Papers
Benjamin C. Pierce University of Pennsylvania
Media Attached
17:50
10m
Other
State of SIGPLAN
Research Papers
Jens Palsberg University of California, Los Angeles (UCLA)
Media Attached
18:15 - 19:15
Reception supported by FacebookResearch Papers at Galeria
18:15
60m
Social Event
Reception supported by Facebook
Research Papers

Fri 18 Jan

Displayed time zone: Belfast change

09:00 - 10:05
SRC Announcement & Keynote IIStudent Research Competition / Research Papers at Sala I + II
Chair(s): Stephanie Weirich University of Pennsylvania, USA
09:00
5m
Awards
SRC Announcement
Student Research Competition
Niki Vazou IMDEA Software Institute
Media Attached
09:05
60m
Talk
Mechanized Metatheory - The Next Chapter
Research Papers
Brigitte Pientka McGill University
Media Attached File Attached
10:35 - 12:03
Abstract InterpretationResearch Papers at Sala II
Chair(s): David Naumann Stevens Institute of Technology
10:35
22m
Talk
A^2 I: Abstract^2 InterpretationDistinguished Paper
Research Papers
Patrick Cousot , Roberto Giacobazzi University of Verona and IMDEA Software Institute, Francesco Ranzato University of Padova
Link to publication DOI Media Attached File Attached
10:57
22m
Talk
Concerto: A Framework for Combined Concrete and Abstract Interpretation
Research Papers
John Toman University of Washington, Seattle, Dan Grossman University of Washington
Link to publication DOI Media Attached
11:19
22m
Talk
Skeletal Semantics and their Interpretations
Research Papers
Martin Bodin Imperial College London, Philippa Gardner Imperial College London, Thomas P. Jensen INRIA Rennes, Alan Schmitt Inria
Link to publication DOI Pre-print Media Attached File Attached
11:41
22m
Talk
Refinement of Path Expressions for Static Analysis
Research Papers
John Cyphert University of Wisconsin - Madison, Jason Breck University of Wisconsin - Madison, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
Link to publication DOI Media Attached File Attached
12:03 - 13:45
12:03
1h42m
Lunch
Lunch
Research Papers

13:45 - 14:51
SemanticsResearch Papers at Sala I
Chair(s): Noam Zeilberger University of Birmingham, UK
13:45
22m
Talk
Better Late Than Never: A Fully Abstract Semantics for Classical Processes
Research Papers
Wen Kokke University of Edinburgh, Fabrizio Montesi University of Southern Denmark, Marco Peressotti University of Southern Denmark
Link to publication DOI Media Attached
14:07
22m
Talk
Diagrammatic Algebra: From Linear to Concurrent Systems
Research Papers
Filippo Bonchi University of Pisa, Joshua Holland University of Southampton, Robin Piedeleu University of Oxford, Pawel Sobocinski University of Southampton, Fabio Zanasi University College London
Link to publication DOI Media Attached
14:29
22m
Talk
Fixpoint Games on Continuous Lattices
Research Papers
Paolo Baldan University of Padova, Barbara König University of Duisburg-Essen, Christina Mika-Michalski University of Duisburg-Essen, Tommaso Padoan University of Padova
Link to publication DOI Media Attached File Attached
13:45 - 14:51
Model CheckingResearch Papers at Sala II
Chair(s): P. Madhusudan University of Illinois at Urbana-Champaign
13:45
22m
Talk
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Research Papers
Taolue Chen Birkbeck, University of London, Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Philipp Ruemmer Uppsala University, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Link to publication DOI Media Attached File Attached
14:07
22m
Talk
Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation
Research Papers
Kyungmin Bae Pohang University of Science and Technology (POSTECH), Jia Lee Pohang University of Science and Technology (POSTECH)
Link to publication DOI Media Attached File Attached
14:29
22m
Talk
Adventures in Monitorability: From Branching to Linear Time and Back Again
Research Papers
Luca Aceto Reykjavik University, Antonis Achilleos Reykjavik University, Adrian Francalanza University of Malta, Anna Ingolfsdottir Reykjavik University, Karoliina Lehtinen University of Kiel and University of Liverpool
Link to publication DOI Media Attached
15:21 - 16:27
Security and Information FlowResearch Papers at Sala I
Chair(s): David Walker Princeton University
15:21
22m
Talk
LWeb: Information Flow Security for Multi-Tier Web Applications
Research Papers
James Parker University of Maryland, Niki Vazou IMDEA Software Institute, Michael Hicks University of Maryland, College Park
Link to publication DOI Media Attached File Attached
15:43
22m
Talk
From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper
Research Papers
Marco Vassena Chalmers University of Technology, Alejandro Russo Chalmers University of Technology, Sweden, Deepak Garg Max Planck Institute for Software Systems, Vineet Rajani MPI-SWS, Deian Stefan University of California San Diego
Link to publication DOI Media Attached File Attached
16:05
22m
Talk
Modalities, Cohesion, and Information Flow
Research Papers
Alex Kavvos Wesleyan University
Link to publication DOI Pre-print File Attached
15:21 - 16:27
Program Analysis IResearch Papers at Sala II
Chair(s): Michael D. Adams University of Utah
15:21
22m
Talk
Decidable Verification of Uninterpreted Programs
Research Papers
Umang Mathur University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
Inferring Frame Conditions with Static Correlation Analysis
Research Papers
Oana-Fabiana Andreescu Internet of Trust, Thomas P. Jensen INRIA Rennes, Stéphane Lescuyer Prove & Run, Benoît Montagu Prove & Run
Link to publication DOI Pre-print Media Attached File Attached
16:05
22m
Talk
Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown SystemsDistinguished Paper
Research Papers
Johannes Späth Fraunhofer IEM, Karim Ali University of Alberta, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
Link to publication DOI Pre-print Media Attached File Attached
16:37 - 17:43
Verified Compilation and ConcurrencyResearch Papers at Sala I
Chair(s): Michael Greenberg Pomona College
16:37
22m
Talk
A Calculus for Esterel: If can, can. If no can, no can.
Research Papers
Spencer P. Florence Northwestern University, USA, Shu-Hung You Northwestern University, USA, Jesse A. Tov Northwestern University, Department of Electrical Engineering and Computer Science, Robert Bruce Findler Northwestern University, USA
Link to publication DOI Media Attached File Attached
16:59
22m
Talk
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Research Papers
Yuting Wang Yale University, Pierre Wilke Yale University, Zhong Shao Yale University
Link to publication DOI Media Attached File Attached
17:21
22m
Talk
A Verified, Efficient Embedding of a Verifiable Assembly Language
Research Papers
Aymeric Fromherz Carnegie Mellon University, Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Bryan Parno , Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
Link to publication DOI Media Attached File Attached
16:37 - 17:43
Program Analysis IIResearch Papers at Sala II
Chair(s): Michael Emmi SRI International
16:37
22m
Talk
Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Research Papers
Xin Yi National University of Defense Technology, Liqian Chen National University of Defense Technology, Xiaoguang Mao National University of Defense Technology, Tao Ji National University of Defense Technology
Link to publication DOI Media Attached File Attached
16:59
22m
Talk
Efficient Parameterized Algorithms for Data Packing
Research Papers
Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady IST Austria, Nastaran Okati Ferdowsi University of Mashhad, Andreas Pavlogiannis EPFL, Switzerland
Link to publication DOI Pre-print Media Attached File Attached
17:21
22m
Talk
Fast and exact analysis for LRU caches
Research Papers
Valentin Touzeau Univ. Grenoble Alpes, Claire Maiza Verimag, France, David Monniaux CNRS, VERIMAG, Jan Reineke Saarland University
Link to publication DOI Media Attached File Attached
17:45 - 18:45
Friday Social HourResearch Papers at Galeria
17:45
60m
Social Event
Social Hour
Research Papers

Accepted Papers

Title
A^2 I: Abstract^2 InterpretationDistinguished Paper
Research Papers
Link to publication DOI Media Attached File Attached
Abstracting Algebraic Effects
Research Papers
Link to publication DOI Media Attached
Abstracting Extensible Data Types; Or, Rows By Any Other Name
Research Papers
Link to publication DOI Media Attached
Abstraction-Safe Effect Handlers via Tunneling
Research Papers
Link to publication DOI Media Attached
A Calculus for Esterel: If can, can. If no can, no can.
Research Papers
Link to publication DOI Media Attached File Attached
A Domain Theory for Statistical Probabilistic ProgrammingDistinguished Paper
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Adventures in Monitorability: From Branching to Linear Time and Back Again
Research Papers
Link to publication DOI Media Attached
An Abstract Domain for Certifying Neural Networks
Research Papers
Link to publication DOI Media Attached
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Research Papers
Link to publication DOI Media Attached File Attached
A Separation Logic for Concurrent Randomized Programs
Research Papers
Link to publication DOI Media Attached File Attached
A True Positives Theorem for a Static Race Detector
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
A Verified, Efficient Embedding of a Verifiable Assembly Language
Research Papers
Link to publication DOI Media Attached File Attached
Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Research Papers
Link to publication DOI Media Attached File Attached
Better Late Than Never: A Fully Abstract Semantics for Classical Processes
Research Papers
Link to publication DOI Media Attached
Bindings as Bounded Natural Functors
Research Papers
Link to publication DOI Media Attached File Attached
Bisimulation as Path Type for Guarded Recursive Types
Research Papers
Link to publication DOI Media Attached File Attached
Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation
Research Papers
Link to publication DOI Media Attached File Attached
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Categorical Combinatorics of Scheduling and Synchronization in Game Semantics
Research Papers
Link to publication DOI Media Attached File Attached
Closed Forms for Numerical Loops
Research Papers
Link to publication DOI Media Attached File Attached
code2vec: Learning Distributed Representations of Code
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Concerto: A Framework for Combined Concrete and Abstract Interpretation
Research Papers
Link to publication DOI Media Attached
Constructing Quotient Inductive-Inductive Types
Research Papers
Link to publication DOI Media Attached File Attached
Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown SystemsDistinguished Paper
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Research Papers
Link to publication DOI Media Attached File Attached
Decidable Verification of Uninterpreted Programs
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Research Papers
Link to publication DOI Media Attached File Attached
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Definitional Proof-Irrelevance without K
Research Papers
Link to publication DOI Media Attached File Attached
Diagrammatic Algebra: From Linear to Concurrent Systems
Research Papers
Link to publication DOI Media Attached
Distributed Programming using Role-Parametric Session Types in Go
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Dynamic Type Inference for Gradual Hindley–Milner Typing
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Research Papers
Link to publication DOI Media Attached File Attached
Efficient Parameterized Algorithms for Data Packing
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Exceptional Asynchronous Session Types: Session Types without Tiers
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Exploring C Semantics and Pointer Provenance
Research Papers
Link to publication DOI Media Attached File Attached
Familial Monads and Structural Operational Semantics
Research Papers
Link to publication DOI Media Attached File Attached
Fast and exact analysis for LRU caches
Research Papers
Link to publication DOI Media Attached File Attached
Fixpoint Games on Continuous Lattices
Research Papers
Link to publication DOI Media Attached File Attached
Formal Verification of Higher-Order Probabilistic Programs
Research Papers
Link to publication DOI Media Attached File Attached
FrAngel: Component-Based Synthesis with Control Structures
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper
Research Papers
Link to publication DOI Media Attached File Attached
Fully Abstract Module Compilation
Research Papers
Link to publication DOI Media Attached File Attached
Game Semantics for Quantum Programming
Research Papers
Link to publication DOI Media Attached
Gradual Parametricity, RevisitedDistinguished Paper
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Gradual Type Theory
Research Papers
Link to publication DOI Media Attached File Attached
Gradual Typing: A New Perspective
Research Papers
Link to publication DOI Media Attached File Attached
Grounding Thin-Air Reads with Event Structures
Research Papers
Link to publication DOI Media Attached File Attached
Hamsaz: Replication Coordination Analysis and Synthesis
Research Papers
Link to publication DOI Media Attached
Higher Inductive Types in Cubical Computational Type Theory
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Inferring Frame Conditions with Static Correlation Analysis
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Intersection Types and Runtime Errors in the Pi-Calculus
Research Papers
Link to publication DOI Media Attached File Attached
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Research Papers
Link to publication DOI Media Attached File Attached
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Research Papers
Link to publication DOI Media Attached File Attached
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
Research Papers
Link to publication DOI Media Attached File Attached
Less is More: Multiparty Session Types Revisited
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Live Functional Programming with Typed Holes
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
LWeb: Information Flow Security for Multi-Tier Web Applications
Research Papers
Link to publication DOI Media Attached File Attached
Modalities, Cohesion, and Information Flow
Research Papers
Link to publication DOI Pre-print File Attached
Modular Quantitative Monitoring
Research Papers
Link to publication DOI Media Attached File Attached
On Library Correctness under Weak Memory Consistency
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Polymorphic Symmetric Multiple Dispatch with Variance
Research Papers
Link to publication DOI Media Attached File Attached
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Research Papers
Link to publication DOI Media Attached
Principality and Approximation under Dimensional Bound
Research Papers
Link to publication DOI Media Attached File Attached
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Quantitative Robustness Analysis of Quantum Programs
Research Papers
Link to publication DOI Media Attached
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Research Papers
Link to publication DOI Media Attached File Attached
Quantum Relational Hoare Logic
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Refinement of Path Expressions for Static Analysis
Research Papers
Link to publication DOI Media Attached File Attached
Skeletal Semantics and their Interpretations
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Research Papers
Link to publication DOI Media Attached
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Research Papers
Link to publication DOI Media Attached File Attached
Structuring the Synthesis of Heap-Manipulating ProgramsDistinguished Paper
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Trace Abstraction Modulo Probability
Research Papers
Link to publication DOI Media Attached
Two sides of the same coin: Session Types and Game Semantics
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Type-Guided Worst-Case Input Generation
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Weak-Consistency Specification via Visibility Relaxation
Research Papers
Link to publication DOI Media Attached File Attached

POPL 2019 Call for Papers

New this year

Scope

The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages. The symposium is sponsored by ACM SIGPLAN, in cooperation with ACM SIGACT and ACM SIGLOG.

Evaluation criteria

The Program Committee will evaluate the technical contribution of each submission as well as its accessibility to both experts and the general POPL audience. All papers will be judged on significance, originality, relevance, correctness, and clarity. Each paper should explain its contributions in both general and technical terms, identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. Authors should strive to make their papers understandable to a broad audience. Advice on writing technical papers can be found on the SIGPLAN author information page.

Evaluation process

Authors will have a multi-day period to respond to reviews, as indicated in the Important Dates table. Responses are optional. They must not be overly long and should not try to introduce new technical results. Reviewers will write a short reaction to these author responses. Following the precedent set by POPL 2018, the program committee will discuss papers entirely electronically rather than at a physical programming committee meeting. This will avoid the time, cost and environmental impact of transporting an increasingly large committee to one point on the globe. Unlike in recent years, there will be no formal External Review Committee, though experts outside the committee will be consulted when their expertise is needed. Reviews will be accompanied by a short summary of the reasons behind the committee’s decision. It is the goal of the program committee to make it clear to the authors why each paper was or was not accepted.

For additional information about the reviewing process, see:

Submission guidelines

Prior to the paper submission deadline, the authors will upload their full anonymized paper. Each paper should have no more than 25 pages of text, excluding bibliography, using the new ACM Proceedings format. This format is chosen for compatibility with PACMPL. It is a single-column page layout with a 10 pt font, 12 pt line spacing, and wider margins than recent POPL page layouts. In this format, the main text block is 5.478 in (13.91 cm) wide and 7.884 in (20.03 cm) tall. Use of a different format (e.g., smaller fonts or a larger text block) is grounds for summary rejection. PACMPL templates for Microsoft Word and LaTeX can be found at the SIGPLAN author information page. In particular, authors using LaTeX should use the acmart-pacmpl-template.tex file (with the acmsmall option). Submissions should be in PDF and printable on both US Letter and A4 paper. Papers may be resubmitted to the submission site multiple times up until the deadline, but the last version submitted before the deadline will be the version reviewed. Papers that exceed the length requirement, that deviate from the expected format, or that are submitted late will be rejected.

Deadlines expire at the end of the day, anywhere on earth on the Important Dates displayed to the right. Submitted papers must adhere to the SIGPLAN Republication Policy and the ACM Policy on Plagiarism. Concurrent submissions to other conferences, workshops, journals, or similar forums of publication are not allowed.

POPL 2019 will employ a lightweight double-blind reviewing process. To facilitate this, submitted papers must adhere to two rules:

  1. author names and institutions must be omitted, and
  2. references to authors’ own related work should be in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”).

The purpose of this process is to help the PC and external reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult. In particular, important background references should not be omitted or anonymized. In addition, authors are free to disseminate their ideas or draft versions of their paper as usual. For example, authors may post drafts of their papers on the web or give talks on their research ideas. A document answering frequently asked questions addresses many common concerns.

The submission itself is the object of review and so it should strive to convince the reader of at least the plausibility of reported results. Still, we encourage authors to provide any supplementary material that is required to support the claims made in the paper, such as detailed proofs, proof scripts, or experimental data. These materials must be uploaded at submission time, as a single pdf or a tarball, not via a URL. Two forms of supplementary material may be submitted.

  1. Anonymous supplementary material is available to the reviewers before they submit their first-draft reviews.
  2. Non-anonymous supplementary material is available to the reviewers after they have submitted their first-draft reviews and learned the identity of the authors.

Use the anonymous form if possible. Reviewers are under no obligation to look at the supplementary material but may refer to it if they have questions about the material in the body of the paper.

Artifact Evaluation

Authors of accepted papers will be invited to formally submit supporting materials to the Artifact Evaluation process. Artifact Evaluation is run by a separate committee whose task is to assess how the artifacts support the work described in the papers. This submission is voluntary and will not influence the final decision regarding the papers. Papers that go through the Artifact Evaluation process successfully will receive a seal of approval printed on the papers themselves. Authors of accepted papers are encouraged to make these materials publicly available upon publication of the proceedings, by including them as “source materials” in the ACM Digital Library.

PACMPL and Copyright

All papers accepted to POPL 2019 will be published as part of the new ACM journal Proceedings of the ACM on Programming Languages (PACMPL). To conform with ACM requirements for journal publication, all POPL papers will be conditionally accepted; authors will be required to submit a short description of the changes made to the final version of the paper, including how the changes address any requirements imposed by the program committee. That the changes are sufficient will be confirmed by the original reviewers prior to acceptance to POPL. Authors of conditionally accepted papers must submit a satisfactory revision to the program committee by the requested deadline or risk rejection.

As a Gold Open Access journal, PACMPL is committed to making peer-reviewed scientific research free of restrictions on both access and (re-)use. Authors are strongly encouraged to support libre open access by licensing their work with the Creative Commons Attribution 4.0 International (CC BY) license, which grants readers liberal (re-)use rights.

Authors of accepted papers will be required to choose one of the following publication rights:

  • Author licenses the work with a Creative Commons license, retains copyright, and (implicitly) grants ACM non-exclusive permission to publish (suggested choice).
  • Author retains copyright of the work and grants ACM a non-exclusive permission to publish license.
  • Author retains copyright of the work and grants ACM an exclusive permission to publish license.
  • Author transfers copyright of the work to ACM.

These choices follow from ACM Copyright Policy and ACM Author Rights, corresponding to ACM’s “author pays” option. While PACMPL may ask authors who have funding for open-access fees to voluntarily cover the article processing charge (currently, US$400), payment is not required for publication. PACMPL and SIGPLAN continue to explore the best models for funding open access, focusing on approaches that are sustainable in the long-term while reducing short-term risk.

Publication and Presentation Requirements

Authors are required to give a short talk (roughly 25 minutes long) at the conference, according to the conference schedule. Papers may not be presented at the conference if they have not been published by ACM under one of the allowed copyright options.

POPL welcomes all authors, regardless of nationality. If authors are unable despite reasonable effort to obtain visas to travel to the conference, arrangements to enable remote participation will be made. In such cases, the general chair, Fritz Henglein, should be contacted for guidance.

All papers will be archived by the ACM Digital Library. Authors will have the option of including supplementary material with their paper.

The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work.

Distinguished Paper Awards

At most 10% of the accepted papers of POPL 2019 will be designated as Distinguished Papers. This award highlights papers that the POPL program committee thinks should be read by a broad audience due to their relevance, originality, significance and clarity. The selection of the distinguished papers will be made based on the final version of the paper and through a second review process.

This FAQ is based on Mike Hicks’ double-blind reviewing FAQ from POPL 2012, lightly-edited and slightly extended by David Walker for POPL 2015 and Andy Gordon for POPL 2017.

General

For authors

For Reviewers

General

Q: Why are you using double-blind reviewing?

A: Our goal is to give each a reviewer an unbiased “first look” at each paper. Studies have shown that a reviewer’s attitude toward a submission may be affected, even unconsciously, by the identity of the author (see link below to more details). We want reviewers to be able to approach each submission without such involuntary reactions as “Barnaby; he writes a good paper” or “Who are these people? I have never heard of them.” For this reason, we ask that authors to omit their names from their submissions, and that they avoid revealing their identity through citation. Note that many systems and security conferences use double-blind reviewing and have done so for years (e.g., SIGCOMM, OSDI, IEEE Security and Privacy, SIGMOD). POPL and PLDI have done it for the last several years.

A key principle to keep in mind is that we intend this process to be cooperative, not adversarial. If a reviewer does discover an author’s identity though a subtle clue or oversight the author will not be penalized.

For those wanting more information, see the list of studies about gender bias in other fields and links to CS-related articles that cover this and other forms of bias below.

Q: Do you really think blinding actually works? I suspect reviewers can often guess who the authors are anyway.

A: Studies of blinding with the flavor we are using show that author identities remain unknown 53% to 79% of the time (see Snodgrass, linked below, for details). Moreover, about 5–10% of the time (again, see Snodgrass), a reviewer is certain of the authors, but then turns out to be at least partially mistaken. So, while sometimes authorship can be guessed correctly, the question is, is imperfect blinding better than no blinding at all? If author names are not explicitly in front of the reviewer on the front page, does that help at all even for the remaining submissions where it would be possible to guess? Our conjecture is that on balance the answer is “yes”.

Q: Couldn’t blind submission create an injustice where a paper is inappropriately rejected based upon supposedly-prior work which was actually by the same authors and not previously published?

A: I have heard of this happening, and this is indeed a serious issue. In the approach we are taking for POPL, author names are revealed to reviewers after they have submitted their review. Therefore, a reviewer can correct their review if they indeed have penalized the authors inappropriately. Unblinding prior to the PC meeting also avoids abuses in which committee members end up advancing the cause of a paper with which they have a conflict.

For authors

Q: What exactly do I have to do to anonymize my paper?

A: Your job is not to make your identity undiscoverable but simply to make it possible for our reviewers to evaluate your submission without having to know who you are. The specific guidelines stated in the call for papers are simple: omit authors’ names from your title page (or list them as “omitted for submission”), and when you cite your own work, refer to it in the third person. For example, if your name is Smith and you have worked on amphibious type systems, instead of saying “We extend our earlier work on statically typed toads (Smith 2004),” you might say “We extend Smith’s (2004) earlier work on statically typed toads.” Also, be sure not to include any acknowledgements that would give away your identity. If you have any questions, feel free to ask the PC chair.

Q: I would like to provide supplementary material for consideration, e.g., the code of my implementation or proofs of theorems. How do I do this?

A: On the submission site there is an option to submit supplementary material along with your main paper. Two forms of supplementary material may be submitted.

Anonymous supplementary material is available to the reviewers before they submit their first-draft reviews. Non-anonymous supplementary material is available to the reviewers only after they have submitted their first-draft reviews and learnt the identity of the authors. Use the anonymous form if possible. Reviewers are under no obligation to look at the supplementary material but may refer to it if they have questions about the material in the body of the paper. The submission itself is the object of review and so it should strive to convince the reader of at least the plausibility of reported results; supplementary material only serves to confirm, in more detail, the idea argued in the paper. Of course, reviewers are free to change their review upon viewing supplementary material (or for any other reason). For those authors who wish to supplement, we encourage them to mention the supplement in the body of the paper so reviewers know to look for it, if necessary. E.g., “The proof of Lemma 1 is included in the non-anonymous supplementary material submitted with this paper.”

Q: Is there a way for me to submit anonymous supplementary material which could be considered by a reviewer before she submits her review (rather than potentially non-anonymous material that can only be viewed afterward) ?

A: Yes, see previous answer. Previously, authors have been known to release a TR, code, etc. via an anonymous hosting service, and to include a URL to that material in the paper. We discourage authors from using such tactics except for materials that cannot, for some reason, be uploaded to the official site (e.g., a live demo). We emphasize that authors should strive to make their paper as convincing as possible within the submission page limit, in case reviewers choose not to access supplementary material. Also, see the next question.

Q: Can I supplement my submission using a URL that links to auxiliary materials instead of submitting such materials to the HotCRP system directly?

A: In general, we discourage authors from providing supplementary materials via links to external web sites. It is possible to change the linked items after the submission deadline has passed, and, to be fair to all authors, we would like to be sure reviewers evaluate materials that have been completed prior to the submission deadline. Having said that, it is appropriate to link to items, such as an online demo, that can’t easily be submitted. Needless to say, attempting to discover the reviewers for your paper by tracking visitors to such a demo site would be a breach of academic integrity. Supplementary items such as PDFs should always be uploaded to HotCRP.

Q: I am building on my own past work on the WizWoz system. Do I need to rename this system in my paper for purposes of anonymity, so as to remove the implied connection between my authorship of past work on this system and my present submission?

A: No. The relationship between systems and authors changes over time, so there will be at least some doubt about authorship. Increasing this doubt by changing the system name would help with anonymity, but it would compromise the research process. In particular, changing the name requires explaining a lot about the system again because you can’t just refer to the existing papers, which use the proper name. Not citing these papers runs the risk of the reviewers who know about the existing system thinking you are replicating earlier work. It is also confusing for the reviewers to read about the paper under Name X and then have the name be changed to Name Y. Will all the reviewers go and re-read the final version with the correct name? If not, they have the wrong name in their heads, which could be harmful in the long run.

Q: I am submitting a paper that extends my own work that previously appeared at a workshop. Should I anonymize any reference to that prior work?

A: No. But we recommend you do not use the same title for your POPL submission, so that it is clearly distinguished from the prior paper. In general there is rarely a good reason to anonymize a citation. One possibility is for work that is tightly related to the present submission and is also under review. But such works may often be non-anonymous. When in doubt, contact the PC Chair.

Q: Am I allowed to post my (non-blinded) paper on my web page? Can I advertise the unblinded version of my paper on mailing lists or send it to colleagues? May I give a talk about my work while it is under review?

A: As far as the authors’ publicity actions are concerned, a paper under double-blind review is largely the same as a paper under regular (single-blind) review. Double-blind reviewing should not hinder the usual communication of results.

That said, we do ask that you not attempt to deliberately subvert the double-blind reviewing process by announcing the names of the authors of your paper to the potential reviewers of your paper. It is difficult to define exactly what counts as “subversion” here, but a blatant example might include sending individual e-mail to members of the PC about your work (unless they are conflicted out anyway). On the other hand, it is perfectly fine, for example, to visit other institutions and give talks about your work, to present your submitted work during job interviews, to present your work at professional meetings (e.g. Dagstuhl), or to post your work on your web page. In general, PC members will not be asked to recuse themselves if they discover the (likely) identity of an author through such means. If you’re not sure about what constitutes “subversion”, please consult directly with the Program Chair.

Q: Will the fact that POPL is double-blind have an impact on handling conflicts-of interest? When I am asked by the submission system to identify conflicts of interest, what criteria should I use?

A: Using DBR does not change the principle that reviewers should not review papers with which they have a conflict of interest, even if they do not immediately know who the authors are. Quoting (with slight alteration) from the ACM SIGPLAN review policies document:

A conflict of interest is defined as a situation in which the reviewer can be viewed as being able to benefit personally in the process of reviewing a paper. For example, if a reviewer is considering a paper written by a member of his own group, a current student, his advisor, or a group that he is seen as being in close competition with, then the outcome of the review process can have direct benefit to the reviewer’s own status. If a conflict of interest exists, the potential reviewer should decline to review the paper.

As an author, you should list PC members (and any others, since others may be asked for outside reviewers) which you believe have a conflict with you. While particular criteria for making this determination may vary, please apply the following guidelines, identifying a potential reviewer Bob as conflicted if

  • Bob was your co-author or collaborator at some point within the last 2 years
  • Bob is an advisor or advisee of yours
  • Bob is a family member
  • Bob has a non-trivial financial stake in your work (e.g., invested in your startup company)

Also please identify institutions with which you are affiliated; all employees or affiliates of these institutions will also be considered conflicted. If a possible reviewer does not meet the above criteria, please do not identify him/her as conflicted. Doing so could be viewed as an attempt to prevent a qualified, but possibly skeptical reviewer from reviewing your paper. If you nevertheless believe that a reviewer who does not meet the above criteria is conflicted, you may identify the person and send a note to the PC Chair.

Q: What happens if the Program Chair has a conflict with the authors of a submitted paper?

A: In general, the Program Chair will designate an alternate to manage the reviewing process for papers with which the Program Chair has a conflict. For POPL 2019, the Program Chair for the next POPL 2020,Lars Birkedal, has agreed to serve in this role.

For reviewers

Q: What should I do if I if I learn the authors’ identity? What should I do if a prospective POPL author contacts me and asks to visit my institution?

A: If at any point you feel that the authors’ actions are largely aimed at ensuring that potential reviewers know their identity, you should contact the Program Chair. Otherwise you should not treat double-blind reviewing differently from regular blind reviewing. In particular, you should refrain from seeking out information on the authors’ identity, but if you discover it accidentally this will not automatically disqualify you as a reviewer. Use your best judgment.

Q: The authors have provided a URL to supplementary material. I would like to see the material but I worry they will snoop my IP address and learn my identity. What should I do?

A: Contact the Program Chair, who will download the material on your behalf and make it available to you.

Q: If I am assigned a paper for which I feel I am not an expert, how do I seek an outside review?

A: PC members should do their own reviews, not delegate them to someone else. If doing so is problematic for some papers, e.g., you don’t feel completely qualified, then consider the following options. First, submit a review for your paper that is as careful as possible, outlining areas where you think your knowledge is lacking. Assuming we have sufficient expert reviews, that could be the end of it: non-expert reviews are valuable too, since conference attendees are by-and-large not experts for any given paper. Second, if you feel like the gaps in your knowledge are substantial, submit a first-cut review, and then work with the PC chair to solicit an external review. This is easy: after submitting your review the paper is unblinded, so you at least know not to solicit the authors! You will also know other reviewers of the paper that have already been solicited. If none of these expert reviewers is acceptable to you, just check with the PC Chair that the person you do wish to solicit is not conflicted with the authors. In addition, the PC chair will attempt to balance the load on external reviewers. Keep in mind that while we would like the PC to make as informed a decision as possible about each submitted paper, each additional review we solicit places a burden on the community.

As a last resort, if you feel like your review would be extremely uninformed and you’d rather not even submit a first cut, contact the PC Chair, and another reviewer will be assigned.

Q: May I ask one of my students to do a review for me?

A: Having students (or interns at a research lab) participate in the review process is good for their education. However, you should not just “offload” your reviews to your students. Each review assigned to you is your responsibility. We recommend the following process: If you are sure that your student’s conflicts of interest are a subset of your own, you and your student may both begin to do your own separate reviews in parallel. (A student’s review should never simply be a substitute for your own work.) If your student’s conflicts of interest are not a subset of your own, you may do your own first-cut review first and then unblind the authors so you can check, or you may consult with the PC chair. Either way, once the student has completed their review, you should check the review to ensure the tone is professional and the content is appropriate. Then you may merge the student’s review with your own.

Q: How do we handle potential conflicts of interest since I cannot see the author names?

A: The conference review system will ask that you identify conflicts of interest when you get an account on the submission system. Please see the related question applied to authors to decide how to identify conflicts. Feel free to also identify additional authors whose papers you feel you could not review fairly for reasons other than those given (e.g., strong personal friendship).

Q: Are PC members allowed to submit papers? If so, how are they handled?

A: PC members are allowed to submit papers. However, since SIGPLAN mandates that PC member papers be held to a “higher standard,” truly borderline PC papers will not receive the benefit of the doubt, whereas a regular non-PC paper might.

Q: How should I handle a paper I feel is very good, and yet would be a better fit for PLDI (or ICFP or OOPSLA)?

A: The scope of POPL is broad and encompasses all topics that pertain to programming language theory, design and implementation. Hence, if you feel a paper would be an excellent PLDI (or ICFP or OOPSLA) paper then it would also be an excellent POPL paper. To be accepted at POPL, a paper must discuss programming languages in some way, shape or form and it must have the potential to make a lasting impact on our field.

Q: How should I handle a paper that is out of scope for POPL?

A: The scope of POPL is broad and encompasses all topics that pertain to programming language theory, design and implementation. However, if you discover you have been assigned a paper that does not contribute to the study of programming languages, please contact the program chair. We will discuss it and may decide to reject the paper on grounds of scope. Of course, if we decide after all that the paper is within the scope of POPL, you should review it like any other paper.

More information about bias in merit reviewing

Note that this information was put together by the program chair; not all program or external review committee members are necessarily persuaded by it.

The 2017 article Effectiveness of Anonymization in Double-Blind Review by Claire Le Goues, Yuriy Brun, Sven Apel, Emery Berger, Sarfraz Khurshid, and Yannis Smaragdakis provides statistics about the use of double-blind reviewing in SIGPLAN conferences. Most reviewers are not able to (correctly) identify the authors of blindly submitted papers.

Kathryn McKinley’s editorial makes the case for double-blind reviewing from a computer science perspective. Her article cites Richard Snodgrass’s SIGMOD record editorial, which collects many studies of the effects of potential bias in peer review.

Here are a few studies on the potential effects of bias manifesting in a merit review process, focusing on bias against women. (These were collected by David Wagner.)

  • There’s the famous story of gender bias in orchestra try-outs, where moving to blind auditions seems to have increased the hiring of female musicians by up to 33% or so. Today some orchestras even go so far as to ask musicians to remove their shoes (or roll out thick carpets) before auditioning, to try to prevent gender-revealing cues from the sound of the auditioner’s shoes.
  • One study found bias in assessment of identical CVs but with names and genders changed. In particular, the researchers mailed out CV’s for a faculty position, but randomly swapped the gender of the name on some of them. They found that both men and women reviewers ranked supposedly-male job applicants higher than supposedly-female applicants – even though the contents of the CV were identical. Presumably, none of the reviewers thought of themselves as biased, yet their evaluations in fact exhibited gender bias. (However: in contrast to the gender bias at hiring time, if the reviewers were instead asked to evaluate whether a candidate should be granted tenure, the big gender differences disappeared. For whatever that’s worth.)
  • The Implicit Association Test illustrates how factors can bias our decision-making, without us realising it. For instance, a large fraction of the population has a tendency to associate men with career (professional life) and women with family (home life), without realizing it. The claim is that we have certain gender stereotypes and schemas which unconsciously influence the way we think. The interesting thing about the IAT is that you can take it yourself. If you want to give it a try, select the Gender-Career IAT or the Gender-Science IAT from here. There’s evidence that these unconscious biases affect our behavior. For instance, one study of recommendation letters written for 300 applicants (looking only at the ones who were eventually hired) found that, when writing about men, letter-writers were more likely to highlight the applicant’s research and technical skills, while when writing about women, letter-writers were more likely to mention the applicant’s teaching and interpersonal skills.
  • There’s a study of postdoctoral funding applications in Sweden, which found that women needed to be about 2.5 times as productive (in terms of papers published) as men, to be ranked equivalently. Other studies have suggested that the Swedish experience may be an anomaly. (For instance, one meta-analysis I saw estimated that, on average, it appears men win about 7% more grant applications than women, but since this is not controlled according to the objective quality of the application, it does not necessarily imply the presence of gender bias in reviewing of grant applications.)
  • This study reports experience from an ecology journal that switched from non-blind to blind reviewing. After the switch, they found a significant (~8%) increase in the acceptance rate for female-first-authored submissions. To put it another way, they saw a 33% increase in the fraction of published papers whose first author is female (28% -> 37%). Keep in mind that this is not a controlled experiment, so it proves correlation but not causation, and there appears to be controversy in the literature about the work. So it is at most a plausibility result that gender bias could be present in the sciences, but far from definitive.

Snodgrass’ studies includes some of these, and more.