Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
POPL 2021 (series) / Online (How to POPL in 2021) /

Room information: POPL-A

VenueOnline (How to POPL in 2021)
Room namePOPL-A
Room InformationNo extra information available
Program

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

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

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

Thu 21 Jan

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

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

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

Fri 22 Jan

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

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

Wed 20 Jan

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

Room16:003017:003018:003019:0030
POPL-A

POPL

Compilers & Optimization

POPL

Program Analysis

Thu 21 Jan

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

Room16:003017:003018:003019:0030
POPL-A

POPL

Security

POPL

Complexity

Fri 22 Jan

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

Room15:003016:003017:003018:0030
POPL-A

POPL

Probabilistic Programming

POPL

Synthesis

Wed 20 Jan

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

Room16:0015304517:0015304518:0015304519:00153045
POPL-A
POPL
Fully Abstract from Static to Gradual
16:00 - 16:10
POPL
Intrinsically Typed Compilation with Nameless Labels
16:10 - 16:20
POPL Distinguished Paper
A Verified Optimizer for Quantum Circuits
16:20 - 16:30
POPL
Verified Code Generation for the Polyhedral Model
16:30 - 16:40
POPL
Formally Verified Speculation and Deoptimization in a JIT Compiler
16:40 - 16:50
POPL
Break
16:50 - 17:00
POPL
Verifying Correct Usage of Context-Free API Protocols
18:30 - 18:40
POPL
Data Flow Refinement Type Inference
18:40 - 18:50
POPL
An Approach to Generate Correctly Rounded Math Libraries for New Floati ...
18:50 - 19:00
POPL Distinguished Paper
An Abstract Interpretation for SPMD Divergence on Reducible Control Flo ...
19:00 - 19:10
POPL
Relatively Complete Verification of Probabilistic Programs
19:10 - 19:20
POPL
A Practical Mode System for Recursive Definitions
19:20 - 19:30

Thu 21 Jan

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

Room16:0015304517:0015304518:0015304519:00153045
POPL-A
POPL
Efficient and Provable Local Capability Revocation using Uninitialized ...
16:00 - 16:10
POPL
Mechanized Logical Relations for Termination-Insensitive Noninterference
16:10 - 16:20
POPL
Giving Semantics to Program-Counter Labels via Secure Effects
16:20 - 16:30
POPL
Automata and Fixpoints for Asynchronous Hyperproperties
16:30 - 16:40
POPL Distinguished Paper
Automatically Eliminating Speculative Leaks from Cryptographic Code wit ...
16:40 - 16:50
POPL
Break
16:50 - 17:00
POPL
Learning the Boundary of Inductive Invariants
18:30 - 18:40
POPL
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
18:40 - 18:50
POPL Distinguished Paper
Context-Bounded Verification of Liveness Properties for Multithreaded S ...
18:50 - 19:00
POPL
Deciding ω-Regular Properties on Linear Recurrence Sequences
19:00 - 19:10
POPL
Deciding Reachability under Persistent x86-TSO
19:10 - 19:20
POPL
On the Complexity of Bidirected Interleaved Dyck-Reachability
19:20 - 19:30

Fri 22 Jan

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

Room15:0015304516:0015304517:0015304518:00153045
POPL-A
POPL
λS: Computable Semantics for Differentiable Programming with Higher-Ord ...
15:45 - 15:55
POPL
Deciding Accuracy of Differential Privacy Schemes
15:55 - 16:05
POPL
Probabilistic Programming Semantics for Name Generation
16:05 - 16:15
POPL
Simplifying Multiple-Statement Reductions with the Polyhedral Model
16:15 - 16:25
POPL Distinguished Paper
A Pre-Expectation Calculus for Probabilistic Sensitivity
16:25 - 16:35
POPL
Paradoxes of probabilistic programming
16:35 - 16:45
POPL
Generating Collection Transformations from Proofs
18:30 - 18:40
POPL
Semantics-Guided Synthesis
18:40 - 18:50
POPL
Combining the Top-down Propagation and Bottom-up Enumeration for Induct ...
18:50 - 19:00