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

Room information: Grand Ballroom A

VenueBoston Park Plaza
Room nameGrand Ballroom A
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

09:00 - 09:10
WelcomePOPL at Grand Ballroom A
Chair(s): Andrew Myers Cornell University, Amal Ahmed Northeastern University, USA
09:10 - 10:15
Invited TalkPOPL at Grand Ballroom A
Chair(s): Amal Ahmed Northeastern University, USA
09:10
65m
Keynote
Principles of Persistent Programming
POPL
Viktor Vafeiadis MPI-SWS
10:45 - 12:00
Automated VerificationPOPL at Grand Ballroom A
Chair(s): Michael Greenberg Stevens Institute of Technology
10:45
25m
Talk
Kater: Automating Weak Memory Model Metatheory and Consistency Checking
POPL
Michalis Kokologiannakis MPI-SWS, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS
DOI
11:10
25m
Talk
Stratified Commutativity in Verification Algorithms for Concurrent ProgramsVirtual
POPL
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg
DOI
11:35
25m
Talk
A Partial Order View of Message-Passing Communication Models
POPL
Cinzia Di Giusto Université Côte d'Azur; CNRS, Davide Ferre' Université Côte d'Azur; CNRS, Laetitia Laversa Université Côte d'Azur; CNRS, Etienne Lozes Université Côte d'Azur; CNRS
DOI
13:30 - 14:45
Logic & Decidability IPOPL at Grand Ballroom A
Chair(s): Zachary Kincaid Princeton University
13:30
25m
Talk
Witnessability of Undecidable Problems
POPL
Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
DOI
13:55
25m
Talk
On the Expressive Power of String Constraints
POPL
Joel D. Day Loughborough University, Vijay Ganesh Georgia Tech, Nathan Grewal University of Waterloo, Florin Manea University of Göttingen
DOI
14:20
25m
Talk
A Robust Theory of Series Parallel Graphs
POPL
Rajeev Alur University of Pennsylvania, Caleb Stanford University of California, San Diego; University of California, Davis, Chris Watson University of Pennsylvania
DOI
15:10 - 16:25
Synthesis IPOPL at Grand Ballroom A
Chair(s): Nadia Polikarpova University of California at San Diego
15:10
25m
Talk
Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
POPL
Woosuk Lee Hanyang University, Hangyeol Cho Hanyang University
DOI
15:35
25m
Talk
FlashFill++: Scaling Programming by Example by Cutting to the Chase
POPL
José Pablo Cambronero Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Daniel Perelman Microsoft, Arjun Radhakrishna Microsoft, Clint Simon Microsoft, Ashish Tiwari Microsoft
DOI
16:00
25m
Talk
Unrealizability Logic
POPL
Jinwoo Kim University of Wisconsin-Madison; Seoul National University, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison
DOI
16:45 - 18:00
Probabilistic InferencePOPL at Grand Ballroom A
Chair(s): Steven Holtzen Northeastern University
16:45
25m
Talk
Affine Monads and Lazy Structures for Bayesian Programming
POPL
Swaraj Dash University of Oxford, Younesse Kaddar University of Oxford, Hugo Paquet University of Oxford, Sam Staton University of Oxford
DOI
17:10
25m
Talk
Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic InferenceVirtual
POPL
Jianlin Li University of Waterloo, Leni Ven University of Waterloo, Pengyuan Shi University of Waterloo, Yizhou Zhang University of Waterloo
DOI
17:35
25m
Talk
Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
POPL
Wonyeol Lee Stanford University, Xavier Rival Inria; ENS; CNRS; PSL University, Hongseok Yang KAIST; IBS
DOI
18:00 - 19:30
SRC PosterStudent Research Competition at Grand Ballroom A
Chair(s): Jeehoon Kang KAIST, Danfeng Zhang Pennsylvania State University
18:00
90m
Talk
Zydeco: A Stack-Based Call-By-Push-Value Language
Student Research Competition
Yuchen Jiang University of Michigan, Runze Xue CSE Department at the University of Michigan
18:00
90m
Talk
HasChor: Choreographic Programming in Haskell
Student Research Competition
Gan Shen University of California, Santa Cruz, USA
18:00
90m
Talk
Towards Synthesis in Superposition
Student Research Competition
Petra Hozzová TU Wien
18:00
90m
Talk
A Formalization of Observational Equivalence in Message Passing Protocols
Student Research Competition
Nathan Liittschwager University of California, Santa Cruz
18:00
90m
Talk
On the metatheory of IRs and the CPS-calculus
Student Research Competition
Paulo Torrens University of Kent
18:00
90m
Talk
Scalable Synthesis of Regular Expressions From Only Positive Examples
Student Research Competition
Elizaveta Pertseva UCSD, Mark Barbone UCSD
18:00
90m
Talk
Evaluating Soundness of a Gradual Verifier with Property Based Testing
Student Research Competition
Jan-Paul Ramos-Davila Cornell University
18:00
90m
Talk
A mechanized model for logical clocks
Student Research Competition
Jonathan Castello UC Santa Cruz
18:00
90m
Talk
Wisening Assertions: A live Bayesian reasoning system for probabilistic correctness
Student Research Competition
Julia Turcotti MIT-CSAIL
18:00
90m
Talk
Synthesizing Vectorized Code via Verified Lifting
Student Research Competition
Jeremy Ferguson University of California-Berkeley
18:00
90m
Talk
Citrus: A Dependently Typed Framework for Pulse-Based Logic
Student Research Competition
Harlan Kringen UC Santa Barbara, Ben Hardekopf University of California at Santa Barbara
18:00
90m
Talk
Neko: A quantum map-filter-reduce programming language
Student Research Competition
Elton Pinto Georgia Institute of Technology
18:00
90m
Talk
Compiling and Running High-level Quantum Programs
Student Research Competition
Hristo Venev INSAIT
18:00
90m
Talk
Trace-Guided Inductive Synthesis of Recursive Functional Programs
Student Research Competition
Yongwei Yuan Purdue University

Thu 19 Jan

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

09:00 - 10:00
Panel: Next 50 Years of POPLPOPL at Grand Ballroom A
Chair(s): Andrew Myers Cornell University
09:00
60m
Panel
Panel: Next 50 Years of POPL
POPL
M: Derek Dreyer MPI-SWS, P: Michael Carbin Massachusetts Institute of Technology, P: Nate Foster Cornell University, P: Xavier Leroy Collège de France, P: Benjamin C. Pierce University of Pennsylvania, P: Nadia Polikarpova University of California at San Diego, P: Azalea Raad Imperial College London, P: Sharon Shoham Tel Aviv University
10:20 - 12:00
Synthesis IIPOPL at Grand Ballroom A
Chair(s): Benjamin Delaware Purdue University
10:20
25m
Talk
babble: Learning Better Abstractions with E-Graphs and Anti-unification
POPL
David Cao University of California at San Diego, Rose Kunkel University of California at San Diego, Chandrakana Nandi Certora, Max Willsey University of Washington, Zachary Tatlock University of Washington, Nadia Polikarpova University of California at San Diego
DOI Pre-print
10:45
25m
Talk
Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
POPL
Ria Das Stanford University, Joshua B. Tenenbaum Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology, Zenna Tavares Basis; Columbia University
DOI
11:10
25m
Talk
Comparative Synthesis: Learning Near-Optimal Network Designs by Query
POPL
Yanjun Wang Amazon Web Services, USA, Zixuan Li Purdue University, Chuan Jiang Purdue University, Xiaokang Qiu Purdue University, Sanjay Rao Purdue University
DOI
11:35
25m
Talk
Top-Down Synthesis for Library Learning
POPL
Maddy Bowers Massachusetts Institute of Technology, Theo X. Olausson Massachusetts Institute of Technology, Lionel Wong Massachusetts Institute of Technology, Gabriel Grand Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Kevin Ellis Cornell University, Armando Solar-Lezama Massachusetts Institute of Technology
DOI Pre-print
13:30 - 14:45
Program Analysis & ParsingPOPL at Grand Ballroom A
Chair(s): David Pichardie Meta
13:30
25m
Talk
SSA Translation Is an Abstract InterpretationDistinguished Paper
POPL
Matthieu Lemerre Université Paris-Saclay - CEA LIST
DOI Pre-print
13:55
25m
Talk
Dynamic Race Detection with O(1) SamplesDistinguished Paper
POPL
Mosaad Al Thokair University of Illinois at Urbana-Champaign, Minjian Zhang University of Illinois at Urbana-Champaign, Umang Mathur National University of Singapore, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
14:20
25m
Talk
Statically Resolvable Ambiguity
POPL
Viktor Palmkvist KTH Royal Institute of Technology, Elias Castegren Uppsala University, Philipp Haller KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology
DOI
15:10 - 16:25
Automatic DifferentiationPOPL at Grand Ballroom A
Chair(s): Ningning Xie University of Toronto
15:10
25m
Talk
You Only Linearize Once: Tangents Transpose to Gradients
POPL
Alexey Radul Google Research, Adam Paszke Google Research, Roy Frostig Google Research, Matthew J. Johnson Google Research, Dougal Maclaurin Google Research
DOI
15:35
25m
Talk
Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
POPL
Tom Smeding Utrecht University, Matthijs Vákár Utrecht University
DOI Pre-print
16:00
25m
Talk
ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic ProgramsDistinguished Paper
POPL
Alexander K. Lew Massachusetts Institute of Technology, Mathieu Huot University of Oxford, Sam Staton University of Oxford, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI Pre-print
16:45 - 18:00
POPL Business MeetingPOPL at Grand Ballroom A

Wed 18 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:0030
Grand Ballroom A

POPL

Welcome

POPL

Invited Talk

POPL

Automated Verification

POPL

Logic & Decidability I

POPL

Synthesis I

POPL

Probabilistic Inference

Student Research Competition

SRC Poster

Thu 19 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Grand Ballroom A

POPL

Panel: Next 50 Years of POPL

POPL

Synthesis II

POPL

Program Analysis & Parsing

POPL

Automatic Differentiation

POPL

POPL Business Meeting

Wed 18 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:00153045
Grand Ballroom A
POPL
Principles of Persistent Programming
09:10 - 10:15
POPL
Kater: Automating Weak Memory Model Metatheory and Consistency Checking
10:45 - 11:10
POPL Virtual
Stratified Commutativity in Verification Algorithms for Concurrent Programs
11:10 - 11:35
POPL
A Partial Order View of Message-Passing Communication Models
11:35 - 12:00
POPL
Witnessability of Undecidable Problems
13:30 - 13:55
POPL
On the Expressive Power of String Constraints
13:55 - 14:20
POPL
A Robust Theory of Series Parallel Graphs
14:20 - 14:45
POPL
Inductive Synthesis of Structurally Recursive Functional Programs from ...
15:10 - 15:35
POPL
FlashFill++: Scaling Programming by Example by Cutting to the Chase
15:35 - 16:00
POPL
Unrealizability Logic
16:00 - 16:25
POPL
Affine Monads and Lazy Structures for Bayesian Programming
16:45 - 17:10
POPL Virtual
Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective ...
17:10 - 17:35
POPL
Smoothness Analysis for Probabilistic Programs with Application to Opti ...
17:35 - 18:00
POPL Student Research Competition
Zydeco: A Stack-Based Call-By-Push-Value Language
18:00 - 19:30
HasChor: Choreographic Programming in Haskell
18:00 - 19:30
Towards Synthesis in Superposition
18:00 - 19:30
A Formalization of Observational Equivalence in Message Passing Protocols
18:00 - 19:30
On the metatheory of IRs and the CPS-calculus
18:00 - 19:30
Scalable Synthesis of Regular Expressions From Only Positive Examples
18:00 - 19:30
Evaluating Soundness of a Gradual Verifier with Property Based Testing
18:00 - 19:30
A mechanized model for logical clocks
18:00 - 19:30
Wisening Assertions: A live Bayesian reasoning system for probabilistic ...
18:00 - 19:30
Synthesizing Vectorized Code via Verified Lifting
18:00 - 19:30
Citrus: A Dependently Typed Framework for Pulse-Based Logic
18:00 - 19:30
Neko: A quantum map-filter-reduce programming language
18:00 - 19:30
Compiling and Running High-level Quantum Programs
18:00 - 19:30
Trace-Guided Inductive Synthesis of Recursive Functional Programs
18:00 - 19:30

Thu 19 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Grand Ballroom A
POPL
Panel: Next 50 Years of POPL
09:00 - 10:00
POPL
babble: Learning Better Abstractions with E-Graphs and Anti-unification
10:20 - 10:45
POPL
Combining Functional and Automata Synthesis to Discover Causal Reactive ...
10:45 - 11:10
POPL
Comparative Synthesis: Learning Near-Optimal Network Designs by Query
11:10 - 11:35
POPL
Top-Down Synthesis for Library Learning
11:35 - 12:00
POPL Distinguished Paper
SSA Translation Is an Abstract Interpretation
13:30 - 13:55
POPL Distinguished Paper
Dynamic Race Detection with O(1) Samples
13:55 - 14:20
POPL
Statically Resolvable Ambiguity
14:20 - 14:45
POPL
You Only Linearize Once: Tangents Transpose to Gradients
15:10 - 15:35
POPL
Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
15:35 - 16:00
POPL Distinguished Paper
ADEV: Sound Automatic Differentiation of Expected Values of Probabilist ...
16:00 - 16:25