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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:15 - 15:45: SocialPOPL at Break
15:15 - 15:45
Social Event
Wednesday Breakfast Tables
POPL
15:45 - 16:00: WelcomePOPL at POPL
15:45 - 16:00
Day opening
Welcome
POPL
16:00 - 17:00: Compilers & OptimizationPOPL at POPL-A
16:00 - 16:10
Talk
Fully Abstract from Static to Gradual
POPL
Koen JacobsKU Leuven, Amin TimanyAarhus University, Dominique DevrieseVrije Universiteit Brussel
Link to publication DOI
16:10 - 16:20
Talk
Intrinsically Typed Compilation with Nameless Labels
POPL
Arjen RouvoetDelft University of Technology, Robbert KrebbersRadboud University Nijmegen, Eelco VisserDelft University of Technology
Link to publication DOI Pre-print
16:20 - 16:30
Talk
A Verified Optimizer for Quantum CircuitsDistinguished Paper
POPL
Kesha HietalaUniversity of Maryland, Robert RandUniversity of Chicago, Shih-Han HungUniversity of Maryland, USA, Xiaodi WuUniversity of Maryland, USA, Michael HicksUniversity of Maryland at College Park
Link to publication DOI
16:30 - 16:40
Talk
Verified Code Generation for the Polyhedral Model
POPL
Nathanaël CourantINRIA, Xavier LeroyCollège de France
Link to publication DOI
16:40 - 16:50
Talk
Formally Verified Speculation and Deoptimization in a JIT Compiler
POPL
Aurèle BarrièreUniv Rennes, IRISA, Sandrine BlazyUniv Rennes, IRISA, Olivier FlückigerNortheastern University, David PichardieUniv Rennes, ENS Rennes, IRISA, Jan VitekNortheastern University / Czech Technical University
Link to publication DOI Pre-print
16:50 - 17:00
Break
Break
POPL
16:00 - 17:00: SemanticsPOPL at POPL-B
16:00 - 16:10
Talk
A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
POPL
Chao-Hong ChenIndiana University, Amr SabryIndiana University
Link to publication DOI
16:10 - 16:20
Talk
Internalizing Representation Independence with Univalence
POPL
Carlo AngiuliCarnegie Mellon University, Evan CavalloCarnegie Mellon University, Anders MörtbergDepartment of Mathematics, Stockholm University, Max ZeunerStockholm University
Link to publication DOI
16:20 - 16:30
Talk
Petr4: Formal Foundations for P4 Data Planes
POPL
Ryan DoengesCornell University, Mina Tahmasbi ArashlooCornell University, Santiago BautistaUniv Rennes, ENS Rennes, Inria, IRISA, Alexander ChangCornell University, Newton NiCornell University, Samwise ParkinsonCornell University, Rudy PetersonCornell University, Alaia Solko-BreslinCornell University, Amanda XuCornell University, Nate FosterCornell University
Link to publication DOI Pre-print
16:30 - 16:40
Talk
The (In)Efficiency of Interaction
POPL
Beniamino AccattoliInria & Ecole Polytechnique, Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Gabriele VanoniUniversity of Bologna & INRIA Sophia Antipolis
Link to publication DOI
16:40 - 16:50
Talk
Functorial Semantics for Partial Theories
POPL
Chad NesterTallinn University of Technology, Ivan Di LibertiCzech Academy of Sciences, Fosco LoregianTallinn University of Technology, Pawel SobocinskiTallinn University of Technology
Link to publication DOI
16:50 - 17:00
Break
Break
POPL
18:00 - 18:30: SocialPOPL at Break
18:30 - 19:30: Program AnalysisPOPL at POPL-A
18:30 - 18:40
Talk
Verifying Correct Usage of Context-Free API Protocols
POPL
Kostas FerlesUT Austin, Jon StephensUniversity of Texas at Austin, Isil DilligUniversity of Texas at Austin
Link to publication DOI
18:40 - 18:50
Talk
Data Flow Refinement Type Inference
POPL
Zvonimir PavlinovicGoogle, USA, Yusen SuNew York University, University of Waterloo, Thomas WiesNew York University, USA
Link to publication DOI
18:50 - 19:00
Talk
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
POPL
Jay P. LimRutgers University, USA, Mridul AanjaneyaRutgers University, John GustafsonNational University of Singapore, Santosh NagarakatteRutgers University, USA
Link to publication DOI
19:00 - 19:10
Talk
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow GraphsDistinguished Paper
POPL
Julian RosemannSaarland University, Saarland Informatics Campus, Simon MollNEC Deutschland, Sebastian HackSaarland University, Germany
Link to publication DOI
19:10 - 19:20
Talk
Relatively Complete Verification of Probabilistic Programs
POPL
Kevin BatzRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University, Germany, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaETH Zurich
Link to publication DOI
19:20 - 19:30
Talk
A Practical Mode System for Recursive Definitions
POPL
Alban ReynaudENS Lyon, Gabriel SchererINRIA Saclay, Jeremy YallopUniversity of Cambridge
Link to publication DOI Pre-print
18:30 - 19:30: Types and Proof AssistancePOPL at POPL-B
18:30 - 18:40
Talk
Asynchronous Effects
POPL
Danel AhmanUniversity of Ljubljana, Matija PretnarUniversity of Ljubljana, Slovenia
Link to publication DOI Pre-print
18:40 - 18:50
Talk
Dijkstra Monads Forever
POPL
Lucas SilverUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
Link to publication DOI
18:50 - 19:00
Talk
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Vineet RajaniMPI-SP, Marco GaboardiBoston University, Deepak GargMax Planck Institute for Software Systems, Jan HoffmannCarnegie Mellon University
Link to publication DOI
19:00 - 19:10
Talk
A Graded Dependent Type System with a Usage-Aware Semantics
POPL
Pritam ChoudhuryUniversity of Pennsylvania, Harley D. Eades IIIAugusta University, Richard A. EisenbergTweag I/O, Stephanie WeirichUniversity of Pennsylvania
Link to publication DOI Pre-print
19:10 - 19:20
Talk
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
POPL
Cameron MoyNortheastern University, Phúc C. NguyễnGoogle, Sam Tobin-HochstadtIndiana University, David Van HornUniversity of Maryland, USA
Link to publication DOI Pre-print
19:20 - 19:30
Talk
The Taming of the Rew: A Type Theory with Computational Assumptions
POPL
Jesper CockxTU Delft, Nicolas TabareauInria, Théo WinterhalterInria — LS2N
Link to publication DOI Pre-print
19:30 - 20:00: SocialPOPL at Break
19:30 - 20:00
Social Event
Happy Hour
POPL
19:30 - 20:00: Sponsor ReceptionPOPL at POPL
19:30 - 20:00
Industry talk
Sponsor Reception
POPL
Media Attached
20:00 - 21:00: SocialPOPL at Break

After Hours

20:00 - 21:00
Social Event
Trivia Night
POPL
20:00 - 20:30: CARESPOPL at CARES

http://sigplan.org/Cares/

20:00 - 20:30
Meeting
SIGPLAN CARES
POPL
P: Stephanie WeirichUniversity of Pennsylvania, P: Alexandra SilvaUniversity College London, P: Shriram KrishnamurthiBrown University, United States, P: David WalkerPrinceton University, USA

Thu 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

02:00 - 03:00: SocialPOPL at Break

After Hours

02:00 - 03:00
Social Event
POPL Cocktail Hour
POPL
04:00 - 04:30: CARESPOPL at CARES

http://sigplan.org/Cares/

04:00 - 04:30
Meeting
SIGPLAN CARES
POPL
P: Stephanie WeirichUniversity of Pennsylvania, P: Hongseok YangKAIST, P: Shriram KrishnamurthiBrown University, United States, P: David WalkerPrinceton University, USA
15:15 - 15:45: SocialPOPL at Break
15:15 - 15:45
Social Event
Topic Oriented Discussions
POPL
15:45 - 15:55: Most Influential POPL PaperPOPL at POPL
15:45 - 15:55
Awards
Most Influential POPL Paper
POPL
Media Attached
16:00 - 17:00: SecurityPOPL at POPL-A
16:00 - 16:10
Talk
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
POPL
Aina Linn GeorgesAarhus University, Armaël GuéneauAarhus University, Thomas Van StrydonckKULeuven, Amin TimanyAarhus University, Alix TrieuAarhus University, Sander HuyghebaertVrije Universiteit Brussel, Dominique DevrieseVrije Universiteit Brussel, Lars BirkedalAarhus University
Link to publication DOI Pre-print
16:10 - 16:20
Talk
Mechanized Logical Relations for Termination-Insensitive Noninterference
POPL
Simon Oddershede GregersenAarhus University, Johan BayAarhus University, Amin TimanyAarhus University, Lars BirkedalAarhus University
Link to publication DOI Pre-print
16:20 - 16:30
Talk
Giving Semantics to Program-Counter Labels via Secure Effects
POPL
Andrew HirschMax Planck Institute for Software Systems, Ethan CecchettiCornell University
Link to publication DOI
16:30 - 16:40
Talk
Automata and Fixpoints for Asynchronous Hyperproperties
POPL
Jens Oliver GutsfeldWestfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-OlmUniversity of Münster, Christoph OhremWestfälische Wilhelms-Universität Münster (WWU), Germany
Link to publication DOI
16:40 - 16:50
Talk
Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper
POPL
Marco VassenaCISPA Helmholtz Center for Information Security, Craig DisselkoenUniversity of California at San Diego, USA, Klaus v. GleissenthallVrije Universiteit Amsterdam, Netherlands, Sunjay CauligiUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, Dean TullsenUniversity of California at San Diego, USA, Deian StefanUniversity of California at San Diego, USA
Link to publication DOI Pre-print
16:50 - 17:00
Break
Break
POPL
16:00 - 17:00: Concurrency (Shared Memory)POPL at POPL-B
16:00 - 16:10
Talk
Verifying Observational Robustness Against a C11-style Memory Model
POPL
Roy MargalitTel Aviv University, Israel, Ori LahavTel Aviv University
Link to publication DOI
16:10 - 16:20
Talk
Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper
POPL
Jatin AroraCMU, Sam WestrickCarnegie Mellon University, Umut A. AcarCarnegie Mellon University
Link to publication DOI
16:20 - 16:30
Talk
Modeling and Analyzing Evaluation Cost of CUDA Kernels
POPL
Stefan K. MullerIllinois Institute of Technology, Jan HoffmannCarnegie Mellon University
Link to publication DOI
16:30 - 16:40
Talk
Optimal Prediction of Synchronization-Preserving Races
POPL
Umang MathurUniversity of Illinois at Urbana-Champaign, Andreas PavlogiannisAarhus University, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
16:40 - 16:50
Talk
Taming x86-TSO Persistency
POPL
Artem KhyzhaTel Aviv University, Ori LahavTel Aviv University
Link to publication DOI Pre-print
16:50 - 17:00
Break
Break
POPL
17:00 - 18:00: Invited TalkPOPL at POPL
17:00 - 18:00
Keynote
Dynamical Systems and Program AnalysisInvited Talk
POPL
James WorrellUniversity of Oxford
File Attached
18:00 - 18:30: SocialPOPL at Break
18:30 - 19:30: ComplexityPOPL at POPL-A
18:30 - 18:40
Talk
Learning the Boundary of Inductive Invariants
POPL
Yotam M. Y. FeldmanTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv University, James R. WilcoxUniversity of Washington
Link to publication DOI
18:40 - 18:50
Talk
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
POPL
Andreas PavlogiannisAarhus University, Anders Alnor MathiasenAarhus University
Link to publication DOI
18:50 - 19:00
Talk
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory ProgramsDistinguished Paper
POPL
Pascal BaumannMax Planck Institute for Software Systems (MPI-SWS), Rupak MajumdarMPI-SWS, Ramanathan S. ThinniyamMax Planck Institute for Software Systems (MPI-SWS), Georg ZetzscheMax Planck Institute for Software Systems (MPI-SWS)
Link to publication DOI
19:00 - 19:10
Talk
Deciding ω-Regular Properties on Linear Recurrence Sequences
POPL
Shaull AlmagorTechnion, Toghrul KarimovMax Planck Institute for Software Systems, Edon KelmendiUniversity of Oxford, Joël OuaknineMax Planck Institute for Software Systems and University of Oxford, James WorrellUniversity of Oxford
Link to publication DOI
19:10 - 19:20
Talk
Deciding Reachability under Persistent x86-TSO
POPL
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Ahmed BouajjaniIRIF, Université Paris Diderot, K Narayan KumarChennai Mathematical Institute, Prakash SaivasanThe Institute of Mathematical Sciences, India
Link to publication DOI
19:20 - 19:30
Talk
On the Complexity of Bidirected Interleaved Dyck-Reachability
POPL
Yuanbo LiGeorgia Institute of Technology, USA, Qirun ZhangGeorgia Institute of Technology, USA, Thomas RepsUniversity of Wisconsin--Madison
Link to publication DOI
18:30 - 19:30: Types and Functional LanguagesPOPL at POPL-B
18:30 - 18:40
Talk
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
POPL
Patrick BahrIT University of Copenhagen, Christian Uldal GraulundIT University of Copenhagen, Rasmus Ejlers MøgelbergIT University of Copenhagen
Link to publication DOI
18:40 - 18:50
Talk
On the Semantic Expressiveness of Recursive Types
POPL
Marco PatrignaniStanford University, USA / CISPA, Germany, Eric Mark MartinStanford, Dominique DevrieseVrije Universiteit Brussel
Link to publication DOI
18:50 - 19:00
Talk
Automatic Differentiation in PCF
POPL
Damiano MazzaCNRS, Michele PaganiIRIF - Université de Paris
Link to publication DOI Pre-print
19:00 - 19:10
Talk
Intersection Types and (Positive) Almost-Sure Termination
POPL
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Claudia FaggianUniversité de Paris & CNRS, Simona Ronchi Della RoccaUniversity of Torino
Link to publication DOI
19:10 - 19:20
Talk
Intensional Datatype Refinement
POPL
Eddie JonesUniversity of Bristol, Steven RamsayUniversity of Bristol
Link to publication DOI
19:20 - 19:30
Talk
Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
POPL
Felipe Bañados SchwerterUniversity of British Columbia, Alison M. ClarkUniversity of British Columbia, Khurram A. JaferyUniversity of British Columbia, Ronald GarciaUniversity of British Columbia
Link to publication DOI
19:30 - 20:30: Business MeetingPOPL at POPL
19:30 - 20:30
Meeting
Business Meeting & Townhall
POPL

Fri 22 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:15 - 15:45: SocialPOPL at Break
15:15 - 15:45
Social Event
Friday Breakfast Tables
POPL
15:45 - 16:45: Probabilistic ProgrammingPOPL at POPL-A
15:45 - 15:55
Talk
λS: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
POPL
Benjamin ShermanMassachusetts Institute of Technology, USA, Jesse MichelMassachusetts Institute of Technology, Michael CarbinMassachusetts Institute of Technology
Link to publication DOI
15:55 - 16:05
Talk
Deciding Accuracy of Differential Privacy Schemes
POPL
Gilles BartheMPI-SP, Germany / IMDEA Software Institute, Spain, Rohit ChadhaUniversity of Missouri, Paul KrogmeierUniversity of Illinois at Urbana-Champaign, A. Prasad SistlaUniversity of Illinois at Chicago, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign
Link to publication DOI
16:05 - 16:15
Talk
Probabilistic Programming Semantics for Name Generation
POPL
Marcin SabokMcGill University, Sam StatonUniversity of Oxford, Dario SteinUniversity of Oxford, Michael WolmanMcGill University
Link to publication DOI Pre-print
16:15 - 16:25
Talk
Simplifying Multiple-Statement Reductions with the Polyhedral Model
POPL
Cambridge YangMIT CSAIL, Eric AtkinsonMIT CSAIL, Michael CarbinMassachusetts Institute of Technology
Link to publication DOI
16:25 - 16:35
Talk
A Pre-Expectation Calculus for Probabilistic SensitivityDistinguished Paper
POPL
Alejandro AguirreIMDEA Software Institute and T.U. of Madrid (UPM), Gilles BartheMPI-SP, Germany / IMDEA Software Institute, Spain, Justin HsuUniversity of Wisconsin-Madison, USA, Benjamin Lucien KaminskiRWTH Aachen University, Germany, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaETH Zurich
Link to publication DOI
16:35 - 16:45
Talk
Paradoxes of probabilistic programming
POPL
Jules JacobsRadboud University Nijmegen
Link to publication DOI Pre-print
15:45 - 16:45: Concurrency (Message Passing)POPL at POPL-B
15:45 - 15:55
Talk
On Algebraic Abstractions for Concurrent Separation Logics
POPL
František FarkaIMDEA Software Institute, Spain, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute, Germán Andrés DelbiancoNomadic Labs, Ignacio FábregasUniversidad Complutense de Madrid
Link to publication DOI
15:55 - 16:05
Talk
Transfinite Step-Indexing for Termination
POPL
Simon SpiesMPI-SWS and University of Cambridge, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Derek DreyerMPI-SWS
Link to publication DOI
16:05 - 16:15
Talk
Precise Subtyping for Asynchronous Multiparty Sessions
POPL
Silvia GhilezanUniversity of Novi Sad, Mathematical Institute SASA, Jovanka PantovićUniversity of Novi Sad, Ivan ProkićUniversity of Novi Sad, Alceste ScalasTechnical University of Denmark, Nobuko YoshidaImperial College London
Link to publication DOI Media Attached
16:15 - 16:25
Talk
A Separation Logic for Effect Handlers
POPL
Link to publication DOI
16:25 - 16:35
Talk
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
POPL
Léon GondelmanAarhus University, Simon Oddershede GregersenAarhus University, Abel NietoAarhus University, Amin TimanyAarhus University, Lars BirkedalAarhus University
Link to publication DOI
16:35 - 16:45
Talk
PerSeVerE: Persistency Semantics for Verification under Ext4
POPL
Michalis KokologiannakisMPI-SWS, Germany, Ilya KaysinNational Research University Higher School of Economics, JetBrains Research, Azalea RaadImperial College London, Viktor VafeiadisMPI-SWS
Link to publication DOI
16:45 - 17:00: BreakPOPL at Break
16:45 - 17:00
Break
Break
POPL
18:00 - 18:30: SocialPOPL at Break
18:30 - 19:00: SynthesisPOPL at POPL-A
18:30 - 18:40
Talk
Generating Collection Transformations from Proofs
POPL
Michael BenediktUniversity of Oxford, UK, Pierre PradicOxford University
Link to publication DOI
18:40 - 18:50
Talk
Semantics-Guided Synthesis
POPL
Jinwoo KimUniversity of Wisconsin-Madison, Qinheping HuUniversity of Wisconsin-Madison, USA, Loris D'AntoniUniversity of Wisconsin-Madison, USA, Thomas RepsUniversity of Wisconsin--Madison
Link to publication DOI
18:50 - 19:00
Talk
Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis
POPL
Woosuk LeeHanyang University, South Korea
Link to publication DOI
18:30 - 19:00: Logic and Decision ProceduresPOPL at POPL-B
18:30 - 18:40
Talk
Cyclic Proofs, System T, and the Power of Contraction
POPL
Denis KuperbergLIP, ENS de Lyon, Laureline PinaultLIP, ENS de Lyon, Damien PousCNRS
Link to publication DOI
18:40 - 18:50
Talk
egg: Fast and Extensible Equality SaturationDistinguished Paper
POPL
Max WillseyUniversity of Washington, USA, Chandrakana NandiUniversity of Washington, USA, Yisu Remy WangUniversity of Washington, Oliver FlattUniversity of Utah, Zachary TatlockUniversity of Washington, Seattle, Pavel PanchekhaUniversity of Utah
Link to publication DOI Pre-print
18:50 - 19:00
Talk
Debugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyTOPLAS
POPL
David ZhaoThe University of Sydney, Pavle SuboticMicrosoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard ScholzUniversity of Sydney, Australia
Link to publication DOI
19:00 - 20:00: Robin Milner AwardPOPL at POPL
19:00 - 20:00
Awards
Robin Milner Award Talk: "Structural Language Models of Code"
POPL
R: Eran YahavTechnion, A: Emery D. BergerUniversity of Massachusetts Amherst
Media Attached
20:00 - 20:30: SocialPOPL at Break

After Hours

20:00 - 20:30
Social Event
Farewell Reception
POPL

Not scheduled yet

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

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.

Accepted Papers

Title
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
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
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Link to publication DOI
A Verified Optimizer for Quantum CircuitsDistinguished Paper
POPL
Link to publication DOI
Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
POPL
Link to publication DOI
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
Asynchronous Effects
POPL
Link to publication DOI Pre-print
Automata and Fixpoints for Asynchronous Hyperproperties
POPL
Link to publication DOI
Automatic Differentiation in PCF
POPL
Link to publication DOI Pre-print
Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper
POPL
Link to publication DOI Pre-print
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
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
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 (In)Efficiency of Interaction
POPL
Link to publication DOI
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
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
egg: Fast and Extensible Equality SaturationDistinguished Paper
POPL
Link to publication DOI Pre-print
λS: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
POPL
Link to publication DOI