POPL 2023
Sun 15 - Sat 21 January 2023 Boston, Massachusetts, United States
POPL 2023 (series) / Boston Park Plaza /

Room information: Avenue34

VenueBoston Park Plaza
Room nameAvenue34
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 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:45 - 12:00
Types IPOPL at Avenue34
Chair(s): Neel Krishnaswami University of Cambridge
10:45
25m
Talk
Higher-Order Leak and Deadlock Free LocksDistinguished Paper
POPL
Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University
DOI
11:10
25m
Talk
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
POPL
Taro Sekiyama National Institute of Informatics, Hiroshi Unno University of Tsukuba; RIKEN AIP
DOI
11:35
25m
Talk
Recursive Subtyping for All
POPL
Litao Zhou University of Hong Kong, Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
13:30 - 14:45
Program Logics & ResourcesPOPL at Avenue34
Chair(s): Robbert Krebbers Radboud University Nijmegen
13:30
25m
Talk
A High-Level Separation Logic for Heap Space under Garbage Collection
POPL
Alexandre Moine Inria, Arthur Charguéraud Inria; Université de Strasbourg; CNRS; ICube, François Pottier Inria
DOI
13:55
25m
Talk
CN: Verifying Systems C Code with Separation-Logic Refinement Types
POPL
Christopher Pulte University of Cambridge, Dhruv C. Makwana University of Cambridge, Thomas Sewell University of Cambridge, Kayvan Memarian University of Cambridge, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge
DOI
14:20
25m
Talk
Conditional Contextual Refinement
POPL
Youngju Song Seoul National University; MPI-SWS, Minki Cho Seoul National University, Dongjae Lee Seoul National University, Chung-Kil Hur Seoul National University, Michael Sammler MPI-SWS, Derek Dreyer MPI-SWS
DOI
15:10 - 16:25
SecurityPOPL at Avenue34
Chair(s): Benjamin C. Pierce University of Pennsylvania
15:10
25m
Talk
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
POPL
Alexandra E. Michael University of California at San Diego; University of Washington, Anitha Gollamudi University of Massachusetts Lowell, Jay Bosamiya Carnegie Mellon University, Evan Johnson University of California at San Diego; Arm, Aidan Denlinger University of California at San Diego, Craig Disselkoen University of California at San Diego, Conrad Watt University of Cambridge, Bryan Parno Carnegie Mellon University, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Deian Stefan University of California at San Diego
DOI
15:35
25m
Talk
Reconciling Shannon and Scott with a Lattice of Computable Information
POPL
Sebastian Hunt City University of London, Dave Sands Chalmers University of Technology, Sandro Stucki Amazon Prime Video
Link to publication DOI Pre-print
16:00
25m
Talk
A Core Calculus for Equational Proofs of Cryptographic Protocols
POPL
Joshua Gancher Carnegie Mellon University, Kristina Sojakova Inria, Xiong Fan Rutgers University, Elaine Shi Carnegie Mellon University, Greg Morrisett Cornell University
DOI
16:45 - 18:00
Verified CompilationPOPL at Avenue34
Chair(s): Ralf Jung ETH Zürich
16:45
25m
Talk
DimSum: A Decentralized Approach to Multi-language Semantics and VerificationDistinguished Paper
POPL
Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Youngju Song Seoul National University; MPI-SWS, Emanuele D’Osualdo MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Deepak Garg MPI-SWS, Derek Dreyer MPI-SWS
DOI
17:10
25m
Talk
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
POPL
Aurèle Barrière University of Rennes; Inria; CNRS; IRISA, Sandrine Blazy University of Rennes; Inria; CNRS; IRISA, David Pichardie Meta
DOI Pre-print
17:35
25m
Talk
Dargent: A Silver Bullet for Verified Data Layout Refinement
POPL
Zilin Chen UNSW, Ambroise Lafont University of Cambridge, Liam O'Connor University of Edinburgh, Gabriele Keller Utrecht University, Craig McLaughlin UNSW, Vincent Jackson University of Melbourne, Christine Rizkallah University of Melbourne
DOI

Thu 19 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 12:00
Semantics IPOPL at Avenue34
Chair(s): Neel Krishnaswami University of Cambridge
10:20
25m
Talk
A Type-Based Approach to Divide-and-Conquer Recursion in Coq
POPL
Pedro da Costa Abreu Junior Purdue University, Benjamin Delaware Purdue University, Alex Hubers University of Iowa, Christa Jenkins University of Iowa, J. Garrett Morris University of Iowa, Aaron Stump University of Iowa
DOI
10:45
25m
Talk
Elements of Quantitative RewritingVirtual
POPL
Francesco Gavazzo University of Pisa, Cecilia Di Florio University of Bologna
DOI
11:10
25m
Talk
The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
POPL
Simon Castellan University of Rennes; Inria; CNRS; IRISA, Pierre Clairambault Université Aix-Marseille; Université de Toulon; CNRS; LIS
DOI
11:35
25m
Talk
Deconstructing the Calculus of Relations with Tape Diagrams
POPL
Filippo Bonchi University of Pisa, Alessandro Di Giorgio University of Pisa, Alessio Santamaria University of Pisa; University of Sussex
DOI
13:30 - 14:45
Resource AnalysisPOPL at Avenue34
Chair(s): Robert Harper Carnegie Mellon University
13:30
25m
Talk
Probabilistic Resource-Aware Session Types
POPL
Ankush Das Amazon, Di Wang Peking University, Jan Hoffmann Carnegie Mellon University
DOI
13:55
25m
Talk
A Calculus for Amortized Expected Runtimes
POPL
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU, Lena Verscht RWTH Aachen University
DOI
14:20
25m
Talk
A General Noninterference Policy for Polynomial Time
POPL
Emmanuel Hainry Université de Lorraine; CNRS; Inria; LORIA, Romain Péchoux Université de Lorraine; CNRS; Inria; LORIA
DOI
15:10 - 16:25
Type TheoryPOPL at Avenue34
Chair(s): Brigitte Pientka McGill University
15:10
25m
Talk
Admissible Types-to-PERs Relativization in Higher-Order LogicDistinguished Paper
POPL
Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen
DOI
15:35
25m
Talk
An Order-Theoretic Analysis of Universe Polymorphism
POPL
Kuen-Bang Hou (Favonia) University of Minnesota, Carlo Angiuli Carnegie Mellon University, Reed Mullanix University of Minnesota
DOI
16:00
25m
Talk
Impredicative Observational Equality
POPL
Loïc Pujet Inria, Nicolas Tabareau Inria
DOI

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:15
Types IIPOPL at Avenue34
Chair(s): Alan Jeffrey Roblox
09:00
25m
Talk
A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
POPL
Nick Rioux University of Pennsylvania, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Steve Zdancewic University of Pennsylvania
DOI
09:25
25m
Talk
Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
POPL
Han Xu Peking University, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
09:50
25m
Talk
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
POPL
Victor Arrial Université Paris Cité - CNRS - IRIF, Giulio Guerrieri Aix Marseille Université - CNRS - LIS; Edinburgh Research Centre - Central Software Institute - Huawei, Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France
DOI
10:45 - 12:00
Semantics & EffectsPOPL at Avenue34
Chair(s): Stephanie Balzer Carnegie Mellon University
10:45
25m
Talk
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
POPL
Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University
DOI
11:10
25m
Talk
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
POPL
Nicolas Chappe University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Paul He University of Pennsylvania, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Steve Zdancewic University of Pennsylvania
DOI
11:35
25m
Talk
Hefty Algebras: Modular Elaboration of Higher-Order Algebraic EffectsRecorded
POPL
Casper Bach Poulsen Delft University of Technology, Cas van der Rest Delft University of Technology
DOI Pre-print
13:30 - 14:45
Formal Methods in Compilation & ImplementationPOPL at Avenue34
Chair(s): Lindsey Kuper University of California at Santa Cruz
13:30
25m
Talk
Tail Recursion Modulo Context: An Equational Approach
POPL
Daan Leijen Microsoft Research, Anton Lorenzen University of Edinburgh
DOI
13:55
25m
Talk
Taking Back Control in an Intermediate Representation for GPU Computing
POPL
Vasileios Klimis Imperial College London, Jack Clark Imperial College London, Alan Baker Google, David Neto Google, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London; Google
DOI
14:20
25m
Talk
Executing Microservice Applications on Serverless, Correctly
POPL
Konstantinos Kallas University of Pennsylvania, Haoran Zhang University of Pennsylvania, Rajeev Alur University of Pennsylvania, Sebastian Angel University of Pennsylvania; Microsoft Research, Vincent Liu University of Pennsylvania
DOI
15:10 - 16:25
Concurrency & LinearizabilityPOPL at Avenue34
Chair(s): Tej Chajed VMware Research
15:10
25m
Talk
An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
POPL
Abhishek Kr Singh Tel Aviv University, Ori Lahav Tel Aviv University
DOI
15:35
25m
Talk
The Path to Durable Linearizability
POPL
Emanuele D’Osualdo MPI-SWS, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS
DOI
16:00
25m
Talk
A Compositional Theory of Linearizability
POPL
Arthur Oliveira Vale Yale University, Zhong Shao Yale University, Yixuan Chen Yale University
DOI
16:45 - 18:00
Semantics IIPOPL at Avenue34
Chair(s): Max S. New University of Michigan
16:45
25m
Talk
Locally Nameless Sets
POPL
Andrew M. Pitts University of Cambridge
DOI Pre-print
17:10
25m
Talk
Why Are Proofs Relevant in Proof-Relevant Models?
POPL
Axel Kerinec Université Sorbonne Paris Nord; LIPN; CNRS, Giulio Manzonetto Université Sorbonne Paris Nord; LIPN; CNRS, Federico Olimpieri University of Leeds
DOI
17:35
25m
Talk
Towards a Higher-Order Mathematical Operational Semantics
POPL
Sergey Goncharov University of Erlangen-Nuremberg, Stefan Milius University of Erlangen-Nuremberg, Lutz Schröder University of Erlangen-Nuremberg, Stelios Tsampas University of Erlangen-Nuremberg, Henning Urbat University of Erlangen-Nuremberg
DOI Pre-print

Sat 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

12:00 - 13:30
LunchPOPL at Avenue34

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Avenue34

POPL

Types I

POPL

Program Logics & Resources

POPL

Security

POPL

Verified Compilation

Thu 19 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room10:003011:003012:003013:003014:003015:003016:0030
Avenue34

POPL

Semantics I

POPL

Resource Analysis

POPL

Type Theory

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Avenue34

POPL

Types II

POPL

Semantics & Effects

POPL

Formal Methods in Compilation & Implementation

POPL

Concurrency & Linearizability

POPL

Semantics II

Sat 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room12:003013:0030
Avenue34

POPL

Lunch

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Avenue34
POPL Distinguished Paper
Higher-Order Leak and Deadlock Free Locks
10:45 - 11:10
POPL
Temporal Verification with Answer-Effect Modification: Dependent Tempor ...
11:10 - 11:35
POPL
Recursive Subtyping for All
11:35 - 12:00
POPL
A High-Level Separation Logic for Heap Space under Garbage Collection
13:30 - 13:55
POPL
CN: Verifying Systems C Code with Separation-Logic Refinement Types
13:55 - 14:20
POPL
Conditional Contextual Refinement
14:20 - 14:45
POPL
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
15:10 - 15:35
POPL
Reconciling Shannon and Scott with a Lattice of Computable Information
15:35 - 16:00
POPL
A Core Calculus for Equational Proofs of Cryptographic Protocols
16:00 - 16:25
POPL Distinguished Paper
DimSum: A Decentralized Approach to Multi-language Semantics and Verifi ...
16:45 - 17:10
POPL
Formally Verified Native Code Generation in an Effectful JIT: Turning t ...
17:10 - 17:35
POPL
Dargent: A Silver Bullet for Verified Data Layout Refinement
17:35 - 18:00

Thu 19 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Avenue34
POPL
A Type-Based Approach to Divide-and-Conquer Recursion in Coq
10:20 - 10:45
POPL Virtual
Elements of Quantitative Rewriting
10:45 - 11:10
POPL
The Geometry of Causality: Multi-token Geometry of Interaction and Its ...
11:10 - 11:35
POPL
Deconstructing the Calculus of Relations with Tape Diagrams
11:35 - 12:00
POPL
Probabilistic Resource-Aware Session Types
13:30 - 13:55
POPL
A Calculus for Amortized Expected Runtimes
13:55 - 14:20
POPL
A General Noninterference Policy for Polynomial Time
14:20 - 14:45
POPL Distinguished Paper
Admissible Types-to-PERs Relativization in Higher-Order Logic
15:10 - 15:35
POPL
An Order-Theoretic Analysis of Universe Polymorphism
15:35 - 16:00
POPL
Impredicative Observational Equality
16:00 - 16:25

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Avenue34
POPL
A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data T ...
09:00 - 09:25
POPL
Making a Type Difference: Subtraction on Intersection Types as Generali ...
09:25 - 09:50
POPL
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Fr ...
09:50 - 10:15
POPL
Step-Indexed Logical Relations for Countable Nondeterminism and Probabi ...
10:45 - 11:10
POPL
Choice Trees: Representing Nondeterministic, Recursive, and Impure Prog ...
11:10 - 11:35
POPL Recorded
Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
11:35 - 12:00
POPL
Tail Recursion Modulo Context: An Equational Approach
13:30 - 13:55
POPL
Taking Back Control in an Intermediate Representation for GPU Computing
13:55 - 14:20
POPL
Executing Microservice Applications on Serverless, Correctly
14:20 - 14:45
POPL
An Operational Approach to Library Abstraction under Relaxed Memory Con ...
15:10 - 15:35
POPL
The Path to Durable Linearizability
15:35 - 16:00
POPL
A Compositional Theory of Linearizability
16:00 - 16:25
POPL
Locally Nameless Sets
16:45 - 17:10
POPL
Why Are Proofs Relevant in Proof-Relevant Models?
17:10 - 17:35
POPL
Towards a Higher-Order Mathematical Operational Semantics
17:35 - 18:00