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

Room information: POPL-B

VenueOnline (How to POPL in 2021)
Room namePOPL-B
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
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: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

Thu 21 Jan

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

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

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

Fri 22 Jan

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

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
Paulo Emílio de Vilhena Inria, François Pottier Inria, France
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
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

Wed 20 Jan

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

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

POPL

Semantics

POPL

Types and Proof Assistance

Thu 21 Jan

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

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

POPL

Concurrency (Shared Memory)

POPL

Types and Functional Languages

Fri 22 Jan

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

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

POPL

Concurrency (Message Passing)

POPL

Logic and Decision Procedures

Wed 20 Jan

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

Room16:0015304517:0015304518:0015304519:00153045
POPL-B
POPL
A Computational Interpretation of Compact Closed Categories: Reversible ...
16:00 - 16:10
POPL
Internalizing Representation Independence with Univalence
16:10 - 16:20
POPL
Petr4: Formal Foundations for P4 Data Planes
16:20 - 16:30
POPL
The (In)Efficiency of Interaction
16:30 - 16:40
POPL
Functorial Semantics for Partial Theories
16:40 - 16:50
POPL
Break
16:50 - 17:00
POPL
Asynchronous Effects
18:30 - 18:40
POPL
Dijkstra Monads Forever
18:40 - 18:50
POPL
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
18:50 - 19:00
POPL
A Graded Dependent Type System with a Usage-Aware Semantics
19:00 - 19:10
POPL
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verific ...
19:10 - 19:20
POPL
The Taming of the Rew: A Type Theory with Computational Assumptions
19:20 - 19:30

Thu 21 Jan

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

Room16:0015304517:0015304518:0015304519:00153045
POPL-B
POPL
Verifying Observational Robustness Against a C11-style Memory Model
16:00 - 16:10
POPL Distinguished Paper
Provably Space Efficient Parallel Functional Programming
16:10 - 16:20
POPL
Modeling and Analyzing Evaluation Cost of CUDA Kernels
16:20 - 16:30
POPL
Optimal Prediction of Synchronization-Preserving Races
16:30 - 16:40
POPL
Taming x86-TSO Persistency
16:40 - 16:50
POPL
Break
16:50 - 17:00
POPL
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded ...
18:30 - 18:40
POPL
On the Semantic Expressiveness of Recursive Types
18:40 - 18:50
POPL
Automatic Differentiation in PCF
18:50 - 19:00
POPL
Intersection Types and (Positive) Almost-Sure Termination
19:00 - 19:10
POPL
Intensional Datatype Refinement
19:10 - 19:20
POPL
Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
19:20 - 19:30

Fri 22 Jan

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

Room15:0015304516:0015304517:0015304518:00153045
POPL-B
POPL
On Algebraic Abstractions for Concurrent Separation Logics
15:45 - 15:55
POPL
Transfinite Step-Indexing for Termination
15:55 - 16:05
POPL
Precise Subtyping for Asynchronous Multiparty Sessions
16:05 - 16:15
POPL
A Separation Logic for Effect Handlers
16:15 - 16:25
POPL
Distributed Causal Memory: Modular Specification and Verification in Hi ...
16:25 - 16:35
POPL
PerSeVerE: Persistency Semantics for Verification under Ext4
16:35 - 16:45
POPL
Cyclic Proofs, System T, and the Power of Contraction
18:30 - 18:40
POPL Distinguished Paper
egg: Fast and Extensible Equality Saturation
18:40 - 18:50
POPL TOPLAS
Debugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy
18:50 - 19:00