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

Room information: Scollay

VenueBoston Park Plaza
Room nameScollay
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

Sun 15 Jan

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

09:00 - 10:30
First SessionLAFI at Scollay
Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6
09:00
5m
Day opening
Opening Comments
LAFI
Christine Tasson Sorbonne Université — LIP6, Steven Holtzen Northeastern University
09:05
60m
Keynote
Introduction to the tensor-programs framework, a PL approach that helps analyse theoretical properties of deep learning.Boston
LAFI
A: Hongseok Yang KAIST; IBS
10:10
10m
Talk
Exact Inference for Discrete Probabilistic Programs via Generating FunctionsParis
LAFI
A: Fabian Zaiser University of Oxford, C.-H. Luke Ong University of Oxford
File Attached
10:20
10m
Talk
Exact Probabilistic Inference Using Generating FunctionsBoston
LAFI
A: Lutz Klinkenberg RWTH Aachen University, Tobias Winkler RWTH Aachen University, Mingshuai Chen RWTH Aachen, Joost-Pieter Katoen RWTH Aachen University
File Attached
11:00 - 12:30
Second SessionLAFI at Scollay
Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6
11:00
20m
Talk
What do posterior distributions of probabilistic programs look like?Boston
LAFI
Mathieu Huot University of Oxford, A: Alexander K. Lew Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Sam Staton University of Oxford
File Attached
11:20
10m
Talk
Semantics of Probabilistic Program TracesBoston
LAFI
Alexander K. Lew Massachusetts Institute of Technology, A: Eli Sennesh Northeastern University, Jan-Willem Van De Meent University of Amsterdam, Vikash Mansinghka Massachusetts Institute of Technology
File Attached
11:30
10m
Talk
A convenient category of tracing measure kernelsBoston
LAFI
A: Eli Sennesh Northeastern University, Jan-Willem Van De Meent University of Amsterdam
File Attached
11:45
5m
Talk
Random probability distributions as natural transformationsParis
LAFI
A: Victor Blanchi ENS Paris, Hugo Paquet University of Oxford
File Attached
11:50
5m
Talk
Static Delayed Sampling for Probabilistic Programming LanguagesParis
LAFI
A: Gizem Caylak KTH Royal Institute of Technology, Daniel Lundén KTH Royal Institute of Technology, Viktor Senderov Naturhistoriska riksmuseet, David Broman KTH Royal Institute of Technology
11:55
5m
Talk
Denotational semantics of languages for inference: semirings, monads, and tensorsOnline
LAFI
Cristina Matache University of Edinburgh, A: Sean Moss University of Oxford, Sam Staton University of Oxford, Ariadne Si Suo University of Oxford
12:10
5m
Talk
Separated and Shared Effects in Higher-Order LanguagesBoston
LAFI
A: Pedro Henrique Azevedo de Amorim Cornell University, Justin Hsu Cornell University
12:15
5m
Talk
On Iteration in Discrete Probabilistic ProgrammingBoston
LAFI
A: Mateo Torres-Ruiz , Robin Piedeleu University of Oxford, Alexandra Silva Cornell University, Fabio Zanasi University College London
File Attached
12:20
5m
Talk
Bit-Blasting Probabilistic ProgramsBoston
LAFI
A: Poorva Garg University of California, Los Angeles, Steven Holtzen Northeastern University, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California at Los Angeles
File Attached
12:25
5m
Talk
πMPC: Automatic Security Proofs for MPC ProtocolsBoston
LAFI
A: Mako P. Bates University of Vermont, Joseph P. Near University of Vermont
14:00 - 15:30
Third SessionLAFI at Scollay
Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6
14:00
20m
Talk
The Variable Elimination Algorithm as a Let-Term RewritingParis
LAFI
Thomas Ehrhard CNRS and University Paris Diderot, Claudia Faggian Université de Paris & CNRS, A: Michele Pagani IRIF - Université de Paris Cité
14:20
20m
Talk
Contextual source code AD transformations for sum typesOnline
LAFI
Adam Paszke Google Research, A: Gordon Plotkin Google
File Attached
14:45
5m
Talk
Pitfalls of Full Bayesian Inference in Universal Probabilistic ProgrammingOnline
LAFI
A: Tim Reichelt University of Oxford, C.-H. Luke Ong University of Oxford, Tom Rainforth Department of Statistics, University of Oxford
File Attached
14:50
5m
Talk
∂ is for Dialectica: typing differentiable programmingOnline
LAFI
A: Marie Kerjean CNRS, Université Sorbonne Paris Nord, Pierre-Marie Pédrot INRIA
15:00
5m
Talk
On the Reparameterisation Gradient for Non-Differentiable but Continuous ModelsBoston
LAFI
C.-H. Luke Ong NTU, A: Dominik Wagner University of Oxford
File Attached
15:05
5m
Talk
Partial Evaluation of Forward-Mode Automatic DifferentiationBoston
LAFI
A: Oscar Eriksson KTH Royal Institute of Technology, Viktor Palmkvist KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology
15:10
5m
Talk
Distribution Theoretic Semantics for Non-Smooth Differentiable ProgrammingBoston
LAFI
Pedro Henrique Azevedo de Amorim Cornell University, A: Christopher Lam University of Illinois at Urbana-Champaign
15:15
5m
Talk
New foundations for probabilistic separation logicBoston
LAFI
A: John Li Northeastern University, Amal Ahmed Northeastern University, USA, Steven Holtzen Northeastern University
File Attached
15:20
5m
Talk
Verified Reversible Programming for Verified Lossless CompressionBoston
LAFI
A: James Townsend University of Amsterdam, Jan-Willem Van De Meent University of Amsterdam
15:25
5m
Talk
Towards type-driven data-science in Idris
LAFI
Ohad Kammar University of Edinburgh, Katarzyna Marek University of Edinburgh, Minh Nguyen University of Bristol, Michel Steuwer University of Edinburgh, Jacob Walters University of Edinburgh, Robert Wright The University of Edinburgh, UK
16:00 - 18:00
Poster SessionLAFI at Scollay
Chair(s): Steven Holtzen Northeastern University

Mon 16 Jan

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

09:00 - 10:30
Tutorials 1ATutorialFest at Scollay
09:00
90m
Tutorial
Z3 Internals – A guide to principles, art and empirics of programming SMT solvers
TutorialFest
Nikolaj Bjørner Microsoft Research
11:00 - 12:30
Tutorials 1BTutorialFest at Scollay
11:00
90m
Tutorial
Z3 Internals – A guide to principles, art and empirics of programming SMT solvers
TutorialFest
Nikolaj Bjørner Microsoft Research
14:00 - 15:30
Tutorials 5ATutorialFest at Scollay
14:00
90m
Tutorial
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
TutorialFest
Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London, Julien Vanegue Bloomberg, USA
16:00 - 17:30
Tutorials 5BTutorialFest at Scollay
16:00
90m
Tutorial
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
TutorialFest
Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London, Julien Vanegue Bloomberg, USA

Tue 17 Jan

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

09:00 - 10:30
Keynote + 1 talkPEPM at Scollay
Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)
09:00
60m
Keynote
Fast Cryptographic Code via Partial Evaluation
PEPM
Adam Chlipala Massachusetts Institute of Technology
10:00
30m
Talk
Towards Type Debugging using Partial Evaluation
PEPM
Kanae Tsushima National Institute of Informatics, Japan, Robert Glück University of Copenhagen
11:00 - 12:30
3 talksPEPM at Scollay
Chair(s): Casper Bach Poulsen Delft University of Technology
11:00
30m
Talk
Semantic Transformation Framework for Rewriting Rules
PEPM
Jihee Park KAIST, Jaemin Hong KAIST, Sukyoung Ryu KAIST
11:30
30m
Talk
Symbolic Execution of Hadamard-Toffoli Quantum Circuits
PEPM
Jacques Carette McMaster University, Gerardo Ortiz Indiana University, Amr Sabry Indiana University
12:00
30m
Talk
Generating Programs for Polynomial Multiplication with Correctness Assurance
PEPM
Ryo Tokuda University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba
14:00 - 15:30
Industry presentation + 1 talkPEPM at Scollay
Chair(s): Sukyoung Ryu KAIST
14:00
60m
Industry talk
MATLAB Coder: Partial Evaluation in Practice
PEPM
Denis Gurchenkov MathWorks, Fred Smith MathWorks
15:00
30m
Talk
Modular Construction of Multi-sorted Free Extensions
PEPM
Guillaume Allais University of St Andrews, Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Nachiappan Valliappan Chalmers University of Technology, Sam Lindley University of Edinburgh, Jeremy Yallop University of Cambridge
File Attached
16:00 - 17:30
2 online talksPEPM at Scollay
Chair(s): Edwin Brady University of St Andrews, UK
16:00
30m
Talk
Efficient Embedding of Strategic Attribute Grammars via MemoizationRemote
PEPM
José Nuno Macedo University of Minho, Emanuel Rodrigues HASLab & INESC TEC, University of Minho, Marcos Viera University of the Republic, Uruguay, João Saraiva
16:30
30m
Talk
Towards a Reflection for Effect HandlersRecorded
PEPM
Youyou Cong Tokyo Institute of Technology, Kenichi Asai Ochanomizu University
17:00
30m
Day closing
Wrap up
PEPM
Jens Palsberg University of California, Los Angeles (UCLA), Edwin Brady University of St Andrews, UK

Sat 21 Jan

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

09:00 - 10:30
Session 1CoqPL at Scollay
09:00
60m
Talk
Omnisemantics: Smooth Handling of Nondeterminism (Invited talk)
CoqPL
Samuel Gruetter Massachusetts Institute of Technology
10:00
30m
Talk
Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching
CoqPL
Xinyi Wan Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University
File Attached
11:00 - 12:30
Session 2CoqPL at Scollay
11:00
30m
Talk
Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation
CoqPL
Dustin Jamner MIT CSAIL, Gabriel Kammer MIT, Adam Chlipala Massachusetts Institute of Technology
File Attached
11:30
30m
Talk
Integrating graphical proofs in Coq
CoqPL
Pablo Donato Ecole polytechnique, Benjamin Werner LIX, IPP, Kaustuv Chaudhuri INRIA & LIX, IPP
File Attached
12:00
30m
Talk
Towards Formally Verified Path ORAM in Coq
CoqPL
Hannah Leung University of Illinois Urbana-Champaign, Talia Ringer University of Illinois at Urbana-Champaign, Christopher W. Fletcher University of Illinois Urbana-Champaign
File Attached
14:00 - 15:30
Session 3CoqPL at Scollay
14:00
30m
Talk
Verified Differential Privacy for Finite Computers
CoqPL
Vivien Rindisbacher Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University
File Attached
14:30
30m
Talk
Formalizing Monoidal Categories and Actions for Syntax with Binders
CoqPL
Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT (CNRS and Univ. of Toulouse), Kobe Wullaert Technical University Delft
File Attached
15:00
30m
Talk
Certifying Complexity Analysis
CoqPL
Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS
File Attached
16:00 - 17:30
Session with the Coq development teamCoqPL at Scollay
16:00
45m
Talk
Session with the Coq Development Team
CoqPL
Yves Bertot INRIA, Maxime Dénès Inria

Sun 15 Jan

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

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

LAFI

First Session

LAFI

Second Session

LAFI

Third Session

LAFI

Poster Session

Mon 16 Jan

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

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

TutorialFest

Tutorials 1A

TutorialFest

TutorialFest

Tutorials 1B

TutorialFest

TutorialFest

Tutorials 5A

TutorialFest

TutorialFest

Tutorials 5B

Tue 17 Jan

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

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

PEPM

Keynote + 1 talk

PEPM

3 talks

PEPM

Industry presentation + 1 talk

PEPM

2 online talks

Sat 21 Jan

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

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

CoqPL

Session 1

CoqPL

Session 2

CoqPL

Session 3

CoqPL

Session with the Coq development team

Sun 15 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:00153045
Scollay
LAFI
Opening Comments
09:00 - 09:05
LAFIBoston
Introduction to the tensor-programs framework, a PL approach that helps ...
09:05 - 10:05
LAFIParis
Exact Inference for Discrete Probabilistic Programs via Generating Func ...
10:10 - 10:20
LAFIBoston
Exact Probabilistic Inference Using Generating Functions
10:20 - 10:30
LAFIBoston
What do posterior distributions of probabilistic programs look like?
11:00 - 11:20
LAFIBoston
Semantics of Probabilistic Program Traces
11:20 - 11:30
LAFIBoston
A convenient category of tracing measure kernels
11:30 - 11:40
LAFIParis
Random probability distributions as natural transformations
11:45 - 11:50
LAFIParis
Static Delayed Sampling for Probabilistic Programming Languages
11:50 - 11:55
LAFIOnline
Denotational semantics of languages for inference: semirings, monads, a ...
11:55 - 12:00
LAFIBoston
Separated and Shared Effects in Higher-Order Languages
12:10 - 12:15
LAFIBoston
On Iteration in Discrete Probabilistic Programming
12:15 - 12:20
LAFIBoston
Bit-Blasting Probabilistic Programs
12:20 - 12:25
LAFIBoston
πMPC: Automatic Security Proofs for MPC Protocols
12:25 - 12:30
LAFIParis
The Variable Elimination Algorithm as a Let-Term Rewriting
14:00 - 14:20
LAFIOnline
Contextual source code AD transformations for sum types
14:20 - 14:40
LAFIOnline
Pitfalls of Full Bayesian Inference in Universal Probabilistic Programming
14:45 - 14:50
LAFIOnline
∂ is for Dialectica: typing differentiable programming
14:50 - 14:55
LAFIBoston
On the Reparameterisation Gradient for Non-Differentiable but Continuou ...
15:00 - 15:05
LAFIBoston
Partial Evaluation of Forward-Mode Automatic Differentiation
15:05 - 15:10
LAFIBoston
Distribution Theoretic Semantics for Non-Smooth Differentiable Programming
15:10 - 15:15
LAFIBoston
New foundations for probabilistic separation logic
15:15 - 15:20
LAFIBoston
Verified Reversible Programming for Verified Lossless Compression
15:20 - 15:25
LAFI
Towards type-driven data-science in Idris
15:25 - 15:30

Mon 16 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Scollay
POPL TutorialFest
Z3 Internals – A guide to principles, art and empirics of programming S ...
09:00 - 10:30
POPL TutorialFest
Z3 Internals – A guide to principles, art and empirics of programming S ...
11:00 - 12:30
POPL TutorialFest
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
14:00 - 15:30
POPL TutorialFest
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
16:00 - 17:30

Tue 17 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Scollay
PEPM
Fast Cryptographic Code via Partial Evaluation
09:00 - 10:00
PEPM
Towards Type Debugging using Partial Evaluation
10:00 - 10:30
PEPM
Semantic Transformation Framework for Rewriting Rules
11:00 - 11:30
PEPM
Symbolic Execution of Hadamard-Toffoli Quantum Circuits
11:30 - 12:00
PEPM
Generating Programs for Polynomial Multiplication with Correctness Assu ...
12:00 - 12:30
PEPM
MATLAB Coder: Partial Evaluation in Practice
14:00 - 15:00
PEPM
Modular Construction of Multi-sorted Free Extensions
15:00 - 15:30
PEPMRemote
Efficient Embedding of Strategic Attribute Grammars via Memoization
16:00 - 16:30
PEPMRecorded
Towards a Reflection for Effect Handlers
16:30 - 17:00
PEPM
Wrap up
17:00 - 17:30

Sat 21 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Scollay
CoqPL
Omnisemantics: Smooth Handling of Nondeterminism (Invited talk)
09:00 - 10:00
CoqPL
Interactive Theorem Proving in Logic Education：A Coq Formalization of Z ...
10:00 - 10:30
CoqPL
Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving C ...
11:00 - 11:30
CoqPL
Integrating graphical proofs in Coq
11:30 - 12:00
CoqPL
Towards Formally Verified Path ORAM in Coq
12:00 - 12:30
CoqPL
Verified Differential Privacy for Finite Computers
14:00 - 14:30
CoqPL
Formalizing Monoidal Categories and Actions for Syntax with Binders
14:30 - 15:00
CoqPL
Certifying Complexity Analysis
15:00 - 15:30
CoqPL
Session with the Coq Development Team
16:00 - 16:45