Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online

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
You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:15 - 15:45
SocialPOPL at Break
15:15
30m
Social Event
Wednesday Breakfast Tables
POPL

15:45 - 16:00
WelcomePOPL at POPL
15:45
15m
Day opening
Welcome
POPL

16:00 - 17:00
Compilers & OptimizationPOPL at POPL-A
16:00
10m
Talk
Fully Abstract from Static to Gradual
POPL
Koen Jacobs KU Leuven, Amin Timany Aarhus University, Dominique Devriese Vrije Universiteit Brussel
Link to publication DOI
16:10
10m
Talk
Intrinsically Typed Compilation with Nameless Labels
POPL
Arjen Rouvoet Delft University of Technology, Robbert Krebbers Radboud University Nijmegen, Eelco Visser Delft University of Technology
Link to publication DOI Pre-print
16:20
10m
Talk
A Verified Optimizer for Quantum CircuitsDistinguished Paper
POPL
Kesha Hietala University of Maryland, Robert Rand University of Chicago, Shih-Han Hung University of Maryland, USA, Xiaodi Wu University of Maryland, USA, Michael Hicks University of Maryland at College Park
Link to publication DOI
16:30
10m
Talk
Verified Code Generation for the Polyhedral Model
POPL
Nathanaël Courant INRIA, Xavier Leroy Collège de France
Link to publication DOI
16:40
10m
Talk
Formally Verified Speculation and Deoptimization in a JIT Compiler
POPL
Aurèle Barrière Univ Rennes, IRISA, Sandrine Blazy Univ Rennes, IRISA, Olivier Flückiger Northeastern University, David Pichardie Univ Rennes, ENS Rennes, IRISA, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL

16:00 - 17:00
SemanticsPOPL at POPL-B
16:00
10m
Talk
A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
POPL
Chao-Hong Chen Indiana University, Amr Sabry Indiana University
Link to publication DOI
16:10
10m
Talk
Internalizing Representation Independence with Univalence
POPL
Carlo Angiuli Carnegie Mellon University, Evan Cavallo Carnegie Mellon University, Anders Mörtberg Department of Mathematics, Stockholm University, Max Zeuner Stockholm University
Link to publication DOI
16:20
10m
Talk
Petr4: Formal Foundations for P4 Data Planes
POPL
Ryan Doenges Cornell University, Mina Tahmasbi Arashloo Cornell University, Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Alexander Chang Cornell University, Newton Ni Cornell University, Samwise Parkinson Cornell University, Rudy Peterson Cornell University, Alaia Solko-Breslin Cornell University, Amanda Xu Cornell University, Nate Foster Cornell University
Link to publication DOI Pre-print
16:30
10m
Talk
The (In)Efficiency of Interaction
POPL
Beniamino Accattoli Inria & Ecole Polytechnique, Ugo Dal Lago University of Bologna, Italy / Inria, France, Gabriele Vanoni University of Bologna & INRIA Sophia Antipolis
Link to publication DOI
16:40
10m
Talk
Functorial Semantics for Partial Theories
POPL
Chad Nester Tallinn University of Technology, Ivan Di Liberti Czech Academy of Sciences, Fosco Loregian Tallinn University of Technology, Pawel Sobocinski Tallinn University of Technology
Link to publication DOI
16:50
10m
Break
Break
POPL

18:00 - 18:30
SocialPOPL at Break
18:30 - 19:30
Program AnalysisPOPL at POPL-A
18:30
10m
Talk
Verifying Correct Usage of Context-Free API Protocols
POPL
Kostas Ferles UT Austin, Jon Stephens University of Texas at Austin, Işıl Dillig University of Texas at Austin
Link to publication DOI
18:40
10m
Talk
Data Flow Refinement Type Inference
POPL
Zvonimir Pavlinovic Google, USA, Yusen Su New York University, University of Waterloo, Thomas Wies New York University, USA
Link to publication DOI
18:50
10m
Talk
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
POPL
Jay P. Lim Rutgers University, USA, Mridul Aanjaneya Rutgers University, John Gustafson National University of Singapore, Santosh Nagarakatte Rutgers University, USA
Link to publication DOI
19:00
10m
Talk
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow GraphsDistinguished Paper
POPL
Julian Rosemann Saarland University, Saarland Informatics Campus, Simon Moll NEC Deutschland, Sebastian Hack Saarland University, Germany
Link to publication DOI
19:10
10m
Talk
Relatively Complete Verification of Probabilistic Programs
POPL
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja ETH Zurich
Link to publication DOI
19:20
10m
Talk
A Practical Mode System for Recursive Definitions
POPL
Alban Reynaud ENS Lyon, Gabriel Scherer INRIA Saclay, Jeremy Yallop University of Cambridge
Link to publication DOI Pre-print
18:30 - 19:30
Types and Proof AssistancePOPL at POPL-B
18:30
10m
Talk
Asynchronous Effects
POPL
Danel Ahman University of Ljubljana, Matija Pretnar University of Ljubljana, Slovenia
Link to publication DOI Pre-print
18:40
10m
Talk
Dijkstra Monads Forever
POPL
Lucas Silver University of Pennsylvania, Steve Zdancewic University of Pennsylvania
Link to publication DOI
18:50
10m
Talk
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Vineet Rajani MPI-SP, Marco Gaboardi Boston University, Deepak Garg Max Planck Institute for Software Systems, Jan Hoffmann Carnegie Mellon University
Link to publication DOI
19:00
10m
Talk
A Graded Dependent Type System with a Usage-Aware Semantics
POPL
Pritam Choudhury University of Pennsylvania, Harley D. Eades III Augusta University, Richard A. Eisenberg Tweag I/O, Stephanie Weirich University of Pennsylvania
Link to publication DOI Pre-print
19:10
10m
Talk
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
POPL
Cameron Moy Northeastern University, Phúc C. Nguyễn Google, Sam Tobin-Hochstadt Indiana University, David Van Horn University of Maryland, USA
Link to publication DOI Pre-print
19:20
10m
Talk
The Taming of the Rew: A Type Theory with Computational Assumptions
POPL
Jesper Cockx TU Delft, Nicolas Tabareau Inria, Théo Winterhalter Inria — LS2N
Link to publication DOI Pre-print
19:30 - 20:00
SocialPOPL at Break
19:30
30m
Social Event
Happy Hour
POPL

19:30 - 20:00
Sponsor ReceptionPOPL at POPL
19:30
30m
Industry talk
Sponsor Reception
POPL

Media Attached
20:00 - 21:00
SocialPOPL at Break

After Hours

20:00
60m
Social Event
Trivia Night
POPL

20:00 - 20:30
20:00
30m
Meeting
SIGPLAN CARES
POPL
P: Stephanie Weirich University of Pennsylvania, P: Alexandra Silva University College London, P: Shriram Krishnamurthi Brown University, United States, P: David Walker Princeton University, USA

Thu 21 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

02:00 - 03:00
SocialPOPL at Break

After Hours

02:00
60m
Social Event
POPL Cocktail Hour
POPL

04:00 - 04:30
04:00
30m
Meeting
SIGPLAN CARES
POPL
P: Stephanie Weirich University of Pennsylvania, P: Hongseok Yang KAIST, P: Shriram Krishnamurthi Brown University, United States, P: David Walker Princeton University, USA
15:15 - 15:45
SocialPOPL at Break
15:15
30m
Social Event
Topic Oriented Discussions
POPL

15:45 - 15:55
Most Influential POPL PaperPOPL at POPL
15:45
10m
Awards
Most Influential POPL Paper
POPL

Media Attached
16:00 - 17:00
SecurityPOPL at POPL-A
16:00
10m
Talk
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
POPL
Aina Linn Georges Aarhus University, Armaël Guéneau Aarhus University, Thomas Van Strydonck KULeuven, Amin Timany Aarhus University, Alix Trieu Aarhus University, Sander Huyghebaert Vrije Universiteit Brussel, Dominique Devriese Vrije Universiteit Brussel, Lars Birkedal Aarhus University
Link to publication DOI Pre-print
16:10
10m
Talk
Mechanized Logical Relations for Termination-Insensitive Noninterference
POPL
Simon Oddershede Gregersen Aarhus University, Johan Bay Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University
Link to publication DOI Pre-print
16:20
10m
Talk
Giving Semantics to Program-Counter Labels via Secure Effects
POPL
Andrew K. Hirsch Max Planck Institute for Software Systems, Ethan Cecchetti Cornell University
Link to publication DOI
16:30
10m
Talk
Automata and Fixpoints for Asynchronous Hyperproperties
POPL
Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-Olm University of Münster, Christoph Ohrem Westfälische Wilhelms-Universität Münster (WWU), Germany
Link to publication DOI
16:40
10m
Talk
Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper
POPL
Marco Vassena CISPA Helmholtz Center for Information Security, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Sunjay Cauligi University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego, USA
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL

16:00 - 17:00
Concurrency (Shared Memory)POPL at POPL-B
16:00
10m
Talk
Verifying Observational Robustness Against a C11-style Memory Model
POPL
Roy Margalit Tel Aviv University, Israel, Ori Lahav Tel Aviv University
Link to publication DOI
16:10
10m
Talk
Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper
POPL
Jatin Arora CMU, Sam Westrick Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
Link to publication DOI
16:20
10m
Talk
Modeling and Analyzing Evaluation Cost of CUDA Kernels
POPL
Stefan K. Muller Illinois Institute of Technology, Jan Hoffmann Carnegie Mellon University
Link to publication DOI
16:30
10m
Talk
Optimal Prediction of Synchronization-Preserving Races
POPL
Umang Mathur University of Illinois at Urbana-Champaign, Andreas Pavlogiannis Aarhus University, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
16:40
10m
Talk
Taming x86-TSO Persistency
POPL
Artem Khyzha Tel Aviv University, Ori Lahav Tel Aviv University
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL

17:00 - 18:00
Invited TalkPOPL at POPL
17:00
60m
Keynote
Dynamical Systems and Program AnalysisInvited Talk
POPL
James Worrell University of Oxford
File Attached
18:00 - 18:30
SocialPOPL at Break
18:30 - 19:30
ComplexityPOPL at POPL-A
18:30
10m
Talk
Learning the Boundary of Inductive Invariants
POPL
Yotam M. Y. Feldman Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv University, James R. Wilcox University of Washington
Link to publication DOI
18:40
10m
Talk
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
POPL
Andreas Pavlogiannis Aarhus University, Anders Alnor Mathiasen Aarhus University
Link to publication DOI
18:50
10m
Talk
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory ProgramsDistinguished Paper
POPL
Pascal Baumann Max Planck Institute for Software Systems (MPI-SWS), Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Max Planck Institute for Software Systems (MPI-SWS), Georg Zetzsche Max Planck Institute for Software Systems (MPI-SWS)
Link to publication DOI
19:00
10m
Talk
Deciding ω-Regular Properties on Linear Recurrence Sequences
POPL
Shaull Almagor Technion, Toghrul Karimov Max Planck Institute for Software Systems, Edon Kelmendi University of Oxford, Joël Ouaknine Max Planck Institute for Software Systems and University of Oxford, James Worrell University of Oxford
Link to publication DOI
19:10
10m
Talk
Deciding Reachability under Persistent x86-TSO
POPL
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Ahmed Bouajjani IRIF, Université Paris Diderot, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan The Institute of Mathematical Sciences, India
Link to publication DOI
19:20
10m
Talk
On the Complexity of Bidirected Interleaved Dyck-Reachability
POPL
Yuanbo Li Georgia Institute of Technology, USA, Qirun Zhang Georgia Institute of Technology, USA, Thomas Reps University of Wisconsin--Madison
Link to publication DOI
18:30 - 19:30
Types and Functional LanguagesPOPL at POPL-B
18:30
10m
Talk
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
POPL
Patrick Bahr IT University of Copenhagen, Christian Uldal Graulund IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen
Link to publication DOI
18:40
10m
Talk
On the Semantic Expressiveness of Recursive Types
POPL
Marco Patrignani Stanford University, USA / CISPA, Germany, Eric Mark Martin Stanford, Dominique Devriese Vrije Universiteit Brussel
Link to publication DOI
18:50
10m
Talk
Automatic Differentiation in PCF
POPL
Damiano Mazza CNRS, Michele Pagani IRIF - Université de Paris
Link to publication DOI Pre-print
19:00
10m
Talk
Intersection Types and (Positive) Almost-Sure Termination
POPL
Ugo Dal Lago University of Bologna, Italy / Inria, France, Claudia Faggian Université de Paris & CNRS, Simona Ronchi Della Rocca University of Torino
Link to publication DOI
19:10
10m
Talk
Intensional Datatype Refinement
POPL
Eddie Jones University of Bristol, Steven Ramsay University of Bristol
Link to publication DOI
19:20
10m
Talk
Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
POPL
Felipe Bañados Schwerter University of British Columbia, Alison M. Clark University of British Columbia, Khurram A. Jafery University of British Columbia, Ronald Garcia University of British Columbia
Link to publication DOI
19:30 - 20:30
Business MeetingPOPL at POPL
19:30
60m
Meeting
Business Meeting & Townhall
POPL

Fri 22 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:15 - 15:45
SocialPOPL at Break
15:15
30m
Social Event
Friday Breakfast Tables
POPL

15:45 - 16:45
Probabilistic ProgrammingPOPL at POPL-A
15:45
10m
Talk
λS: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
POPL
Benjamin Sherman Massachusetts Institute of Technology, USA, Jesse Michel Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI
15:55
10m
Talk
Deciding Accuracy of Differential Privacy Schemes
POPL
Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Rohit Chadha University of Missouri, Paul Krogmeier University of Illinois at Urbana-Champaign, A. Prasad Sistla University of Illinois at Chicago, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI
16:05
10m
Talk
Probabilistic Programming Semantics for Name Generation
POPL
Marcin Sabok McGill University, Sam Staton University of Oxford, Dario Stein University of Oxford, Michael Wolman McGill University
Link to publication DOI Pre-print
16:15
10m
Talk
Simplifying Multiple-Statement Reductions with the Polyhedral Model
POPL
Cambridge Yang MIT CSAIL, Eric Atkinson MIT CSAIL, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI
16:25
10m
Talk
A Pre-Expectation Calculus for Probabilistic SensitivityDistinguished Paper
POPL
Alejandro Aguirre IMDEA Software Institute and T.U. of Madrid (UPM), Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Justin Hsu University of Wisconsin-Madison, USA, Benjamin Lucien Kaminski RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja ETH Zurich
Link to publication DOI
16:35
10m
Talk
Paradoxes of probabilistic programming
POPL
Jules Jacobs Radboud University Nijmegen
Link to publication DOI Pre-print
15:45 - 16:45
Concurrency (Message Passing)POPL at POPL-B
15:45
10m
Talk
On Algebraic Abstractions for Concurrent Separation Logics
POPL
František Farka IMDEA Software Institute, Spain, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute, Germán Andrés Delbianco Nomadic Labs, Ignacio Fábregas Universidad Complutense de Madrid
Link to publication DOI
15:55
10m
Talk
Transfinite Step-Indexing for Termination
POPL
Simon Spies MPI-SWS and University of Cambridge, Neel Krishnaswami Computer Laboratory, University of Cambridge, Derek Dreyer MPI-SWS
Link to publication DOI
16:05
10m
Talk
Precise Subtyping for Asynchronous Multiparty Sessions
POPL
Silvia Ghilezan University of Novi Sad, Mathematical Institute SASA, Jovanka Pantović University of Novi Sad, Ivan Prokić University of Novi Sad, Alceste Scalas Technical University of Denmark, Nobuko Yoshida Imperial College London
Link to publication DOI Media Attached
16:15
10m
Talk
A Separation Logic for Effect Handlers
POPL
Link to publication DOI
16:25
10m
Talk
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
POPL
Léon Gondelman Aarhus University, Simon Oddershede Gregersen Aarhus University, Abel Nieto Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University
Link to publication DOI
16:35
10m
Talk
PerSeVerE: Persistency Semantics for Verification under Ext4
POPL
Michalis Kokologiannakis MPI-SWS, Germany, Ilya Kaysin National Research University Higher School of Economics, JetBrains Research, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS
Link to publication DOI
16:45 - 17:00
BreakPOPL at Break
16:45
15m
Break
Break
POPL

18:00 - 18:30
SocialPOPL at Break
18:30 - 19:00
SynthesisPOPL at POPL-A
18:30
10m
Talk
Generating Collection Transformations from Proofs
POPL
Michael Benedikt University of Oxford, UK, Pierre Pradic Oxford University
Link to publication DOI
18:40
10m
Talk
Semantics-Guided Synthesis
POPL
Jinwoo Kim University of Wisconsin-Madison, Qinheping Hu University of Wisconsin-Madison, USA, Loris D'Antoni University of Wisconsin-Madison, USA, Thomas Reps University of Wisconsin--Madison
Link to publication DOI
18:50
10m
Talk
Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis
POPL
Woosuk Lee Hanyang University, South Korea
Link to publication DOI
18:30 - 19:00
Logic and Decision ProceduresPOPL at POPL-B
18:30
10m
Talk
Cyclic Proofs, System T, and the Power of Contraction
POPL
Denis Kuperberg LIP, ENS de Lyon, Laureline Pinault LIP, ENS de Lyon, Damien Pous CNRS
Link to publication DOI
18:40
10m
Talk
egg: Fast and Extensible Equality SaturationDistinguished Paper
POPL
Max Willsey University of Washington, USA, Chandrakana Nandi University of Washington, USA, Yisu Remy Wang University of Washington, Oliver Flatt University of Utah, Zachary Tatlock University of Washington, Seattle, Pavel Panchekha University of Utah
Link to publication DOI Pre-print
18:50
10m
Talk
Debugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyTOPLAS
POPL
David Zhao The University of Sydney, Pavle Subotic Microsoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard Scholz University of Sydney, Australia
Link to publication DOI
19:00 - 20:00
Robin Milner AwardPOPL at POPL
19:00
60m
Awards
Robin Milner Award Talk: "Structural Language Models of Code"
POPL
R: Eran Yahav Technion, A: Emery D. Berger University of Massachusetts Amherst
Media Attached
20:00 - 20:30
SocialPOPL at Break

After Hours

20:00
30m
Social Event
Farewell Reception
POPL

Unscheduled Events

Not scheduled
Social Event
Structured Social
POPL

Not scheduled
Talk
Abstracting Large-scale Datalog: A Scalable Provenance Evaluation Strategy
POPL
David Zhao The University of Sydney, Pavle Subotic Microsoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard Scholz The University of Sydney
Link to publication DOI
Not scheduled
Social Event
Coffee Break
POPL

Accepted Papers

Title
Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
POPL
Link to publication DOI
A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
POPL
Link to publication DOI
A Graded Dependent Type System with a Usage-Aware Semantics
POPL
Link to publication DOI Pre-print
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow GraphsDistinguished Paper
POPL
Link to publication DOI
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
POPL
Link to publication DOI
A Practical Mode System for Recursive Definitions
POPL
Link to publication DOI Pre-print
A Pre-Expectation Calculus for Probabilistic SensitivityDistinguished Paper
POPL
Link to publication DOI
A Separation Logic for Effect Handlers
POPL
Link to publication DOI
Asynchronous Effects
POPL
Link to publication DOI Pre-print
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Link to publication DOI
Automata and Fixpoints for Asynchronous Hyperproperties
POPL
Link to publication DOI
Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper
POPL
Link to publication DOI Pre-print
Automatic Differentiation in PCF
POPL
Link to publication DOI Pre-print
A Verified Optimizer for Quantum CircuitsDistinguished Paper
POPL
Link to publication DOI
Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis
POPL
Link to publication DOI
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory ProgramsDistinguished Paper
POPL
Link to publication DOI
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
POPL
Link to publication DOI Pre-print
Cyclic Proofs, System T, and the Power of Contraction
POPL
Link to publication DOI
Data Flow Refinement Type Inference
POPL
Link to publication DOI
Deciding Accuracy of Differential Privacy Schemes
POPL
Link to publication DOI
Deciding Reachability under Persistent x86-TSO
POPL
Link to publication DOI
Deciding ω-Regular Properties on Linear Recurrence Sequences
POPL
Link to publication DOI
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
POPL
Link to publication DOI
Dijkstra Monads Forever
POPL
Link to publication DOI
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
POPL
Link to publication DOI
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
POPL
Link to publication DOI Pre-print
egg: Fast and Extensible Equality SaturationDistinguished Paper
POPL
Link to publication DOI Pre-print
Formally Verified Speculation and Deoptimization in a JIT Compiler
POPL
Link to publication DOI Pre-print
Fully Abstract from Static to Gradual
POPL
Link to publication DOI
Functorial Semantics for Partial Theories
POPL
Link to publication DOI
Generating Collection Transformations from Proofs
POPL
Link to publication DOI
Giving Semantics to Program-Counter Labels via Secure Effects
POPL
Link to publication DOI
Intensional Datatype Refinement
POPL
Link to publication DOI
Internalizing Representation Independence with Univalence
POPL
Link to publication DOI
Intersection Types and (Positive) Almost-Sure Termination
POPL
Link to publication DOI
Intrinsically Typed Compilation with Nameless Labels
POPL
Link to publication DOI Pre-print
Learning the Boundary of Inductive Invariants
POPL
Link to publication DOI
Mechanized Logical Relations for Termination-Insensitive Noninterference
POPL
Link to publication DOI Pre-print
Modeling and Analyzing Evaluation Cost of CUDA Kernels
POPL
Link to publication DOI
On Algebraic Abstractions for Concurrent Separation Logics
POPL
Link to publication DOI
On the Complexity of Bidirected Interleaved Dyck-Reachability
POPL
Link to publication DOI
On the Semantic Expressiveness of Recursive Types
POPL
Link to publication DOI
Optimal Prediction of Synchronization-Preserving Races
POPL
Link to publication DOI Pre-print
Paradoxes of probabilistic programming
POPL
Link to publication DOI Pre-print
PerSeVerE: Persistency Semantics for Verification under Ext4
POPL
Link to publication DOI
Petr4: Formal Foundations for P4 Data Planes
POPL
Link to publication DOI Pre-print
Precise Subtyping for Asynchronous Multiparty Sessions
POPL
Link to publication DOI Media Attached
Probabilistic Programming Semantics for Name Generation
POPL
Link to publication DOI Pre-print
Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper
POPL
Link to publication DOI
Relatively Complete Verification of Probabilistic Programs
POPL
Link to publication DOI
λS: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
POPL
Link to publication DOI
Semantics-Guided Synthesis
POPL
Link to publication DOI
Simplifying Multiple-Statement Reductions with the Polyhedral Model
POPL
Link to publication DOI
Taming x86-TSO Persistency
POPL
Link to publication DOI Pre-print
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
POPL
Link to publication DOI
The (In)Efficiency of Interaction
POPL
Link to publication DOI
The Taming of the Rew: A Type Theory with Computational Assumptions
POPL
Link to publication DOI Pre-print
Transfinite Step-Indexing for Termination
POPL
Link to publication DOI
Verified Code Generation for the Polyhedral Model
POPL
Link to publication DOI
Verifying Correct Usage of Context-Free API Protocols
POPL
Link to publication DOI
Verifying Observational Robustness Against a C11-style Memory Model
POPL
Link to publication DOI

POPL 2021 Call for Papers

POPL 2021 will welcome contributions from all members of the community. Independent of what will happen with global Covid-19 crisis and the complications of its aftermath, authors and other participants will be given the choice to participate in-person or remotely.

The paper submission deadline (July 9, 2020) is firm and not subject to change.

POPL will take place January 17-22, 2021, as a physical, virtual, or hybrid physical/virtual meeting. We will be monitoring the Covid-19 situation and will announce a decision on the nature of the meeting in time.

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 must explain its scientific contribution in both general and technical terms, identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. 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. A response must be concise, addressing specific points raised in review; in particular, it must not introduce new technical results. Reviewers will write a short reaction to these author responses. 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. There is no formal External Review Committee, though experts outside the committee will be consulted. Reviews will be accompanied by a short summary of the reasons behind the committee’s decision with the goal of clarifying the reasons behind the decision.

For additional information about the reviewing process, see:

Submission guidelines

The following two points are easy to overlook:

  • Conflicts: Each author of a submission has to log into the submission system and properly declare all potential conflicts of interest in the author profile form. A conflict caught late in the reviewing process leads to a voided review which may be infeasible to replace.
  • Anonymity: POPL 2021 will employ a lightweight double-blind reviewing process. Make sure that your submitted paper is fully anonymized.

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 2021 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 2021 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

Papers may not be presented at the conference if they have not been published by ACM under one of the allowed copyright options. 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.

Authors of accepted papers are required to give a short talk (roughly 25 minutes long) at the conference, according to the conference schedule. Presentations will not take the traditional ~25min slots, since POPL 2021 is a virtual conference. Authors will be pre-recording talks; instructions will be sent to corresponding authors soon.

Distinguished Paper Awards

At most 10% of the accepted papers of POPL 2021 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.