PriSC 2023
Sun 15 - Sat 21 January 2023 Boston, Massachusetts, United States
co-located with POPL 2023
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

14:00 - 15:30
Tutorials 5APOPL TutorialFest at Scollay
14:00
90m
Tutorial
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
POPL 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 5BPOPL TutorialFest at Scollay
16:00
90m
Tutorial
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
POPL 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

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

Sun 15 Jan

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

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

Mon 16 Jan

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

Tue 17 Jan

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

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

Sat 21 Jan

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

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

Sun 15 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:00153045
Scollay