Semantics of Probabilistic Program Traces (LAFI 2023) - POPL 2023

Sun 15 - Sat 21 January 2023 Boston, Massachusetts, United States

Who

Alexander K. Lew, Eli Sennesh, Jan-Willem Van De Meent, Vikash Mansinghka

Track

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

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 programSpecify a time band

When

Sun 15 Jan 2023 11:20 - 11:30 at Scollay - Second Session Chair(s): Steven Holtzen, Christine Tasson

Abstract

This extended abstract presents a minimal core calculus modeling modern, trace-based PPLs–PPLs like Gen, ProbTorch, Pyro, and Turing in which probabilistic program traces are not just an implementation detail, but rather a user-facing data type, meant to be inspected and explicitly reasoned about. We show how to precisely define the distribution a program encodes over traces, and illustrate how to define and validate program transformations using the calculus (our example transformations are for computing trace densities and implementing weighted samplers). Our aim is to: (1) give theorists a self-contained model of a typical trace-based PPL, to facilitate discussions between implementors/users of such languages and PPL theorists; (2) give PPL developers a blueprint for formal reasoning about program semantics & new program transformations, and (3) provide a common reference point for discussion and comparison of many real-world PPLs.

File attachments

Semantics of Probabilistic Program Traces (lafi23-final97.pdf)	542KiB

Alexander K. Lew

Massachusetts Institute of Technology

United States

Eli SenneshAuthor

Northeastern University

United States

Jan-Willem Van De Meent

University of Amsterdam

Vikash Mansinghka

Massachusetts Institute of Technology

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

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 programSpecify a time band

Session Program

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

	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