Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
VenueOnline (How to POPL in 2021)
Room namePOPL-B
Additional informationThere is no additional information of this room 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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

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

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

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

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

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

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

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