PLMW 2021
Mon 18 - Tue 19 January 2021
Online
co-located with
POPL 2021
Toggle navigation
Attending
Venue: Online (How to POPL in 2021)
Program
Complete Program
Your Program
Mon 18 Jan
Tue 19 Jan
Track/Call
Organization
PLMW 2021 Committees
Track Committees
Invited Speakers
Panelists
Organizing Committee
Contributors
People Index
Search
Series
Series
PLMW @ ICFP 2024
PLMW@PLDI 2024
PLMW @ POPL 2024
PLMW @ ICFP 2023
PLMW @ POPL 2023
PLMW@PLDI 2023
PLMW @ ICFP 2022
PLMW
PLMW 2022
PLMW @ ICFP 2021
PLMW@PLDI 2021
PLMW 2021
PLMW @ ICFP 2020
PLMW@PLDI 2020
PLMW 2020
PLMW @ ICFP 2019
PLMW @ PLDI 2019
PLMW 2019
PLMW @ ICFP 2018
PLMW @ PLDI 2018
PLMW 2018
PLMW 2017
PLMW 2017
PLMW
PLMW 2016
PLMW@PLDI
PLMW
Sign in
Sign up
POPL 2021
(
series
) /
PLMW 2021 (
series
) /
Online (How to POPL in 2021)
/
Room information: POPL-B
Venue
Online (How to POPL in 2021)
Room name
POPL-B
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
.
Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
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
Semantics
POPL
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 Assistance
POPL
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
,
Theo 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 Programming
Distinguished 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 Languages
POPL
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 Procedures
POPL
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 Saturation
Distinguished 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 Strategy
TOPLAS
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
Room
16:00
30
17:00
30
18:00
30
19:00
30
POPL-B
POPL
Semantics
POPL
Types and Proof Assistance
Thu 21 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
16:00
30
17:00
30
18:00
30
19:00
30
POPL-B
POPL
Concurrency (Shared Memory)
POPL
Types and Functional Languages
Fri 22 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
15:00
30
16:00
30
17:00
30
18:00
30
POPL-B
POPL
Concurrency (Message Passing)
POPL
Logic and Decision Procedures
Wed 20 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
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
Room
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
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
Room
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
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
x
Sat 20 Apr 00:17