PEPM 2023
Tue 17 Jan 2023
Boston, Massachusetts, United States
co-located with
POPL 2023
Toggle navigation
Attending
Venue: Boston Park Plaza
Program
Complete Program
Your Program
Tue 17 Jan
Track/Call
Organization
PEPM 2023 Committees
Track Committees
Organizing Committee
Program Committee
Steering Committee
Contributors
People Index
Search
Series
Series
PEPM 2024
PEPM 2023
PEPM 2022
PEPM 2021
PEPM 2020
PEPM 2019
PEPM 2018
PEPM 2017
PEPM 2016
PEPM 2015
Sign in
Sign up
POPL 2023
(
series
) /
PEPM 2023 (
series
) /
Boston Park Plaza
/
Room information: Avenue34
Venue
Boston Park Plaza
Room name
Avenue34
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-05:00) Eastern Time (US & Canada)
.
Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)
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-06: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+03: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 18 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
10:45 - 12:00
Types I
POPL
at
Avenue34
Chair(s):
Neel Krishnaswami
University of Cambridge
10:45
25m
Talk
Higher-Order Leak and Deadlock Free Locks
Distinguished 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 & Resources
POPL
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
Security
POPL
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 Compilation
POPL
at
Avenue34
Chair(s):
Ralf Jung
ETH Zürich
16:45
25m
Talk
DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Distinguished 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 I
POPL
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 Rewriting
Virtual
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 Analysis
POPL
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 Theory
POPL
at
Avenue34
Chair(s):
Brigitte Pientka
McGill University
15:10
25m
Talk
Admissible Types-to-PERs Relativization in Higher-Order Logic
Distinguished 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 II
POPL
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 & Effects
POPL
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 Effects
Recorded
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 & Implementation
POPL
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 & Linearizability
POPL
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 II
POPL
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
Lunch
POPL
at
Avenue34
Wed 18 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Avenue34
POPL
Types I
POPL
Program Logics & Resources
POPL
Security
POPL
Verified Compilation
Thu 19 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
Avenue34
POPL
Semantics I
POPL
Resource Analysis
POPL
Type Theory
Fri 20 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
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
Room
12:00
30
13:00
30
Avenue34
POPL
Lunch
Wed 18 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
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
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
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
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
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
x
Sat 20 Apr 00:45