LAFI 2023
who it's for
probabilistic programming researchers, programming language researchers, machine learning researchers, compiler developers, formal verification engineers, security and MPC researchers, applied Bayesian statisticians
topics
tensor programs framework and infinite-width GPs; probability generating function inference; generating-function loop semantics; trace semantics in quasi-Borel spaces; static delayed sampling compilation; forward-mode automatic differentiation partial evaluation; reparameterisation gradients for non-smooth models; distribution-theoretic semantics for piecewise analytic programs; bit-blasting reals to discrete bits; variable elimination as let-term rewriting; denotational semirings and monads for PPLs; verified reversible programming for compression
| title | author | length |
|---|---|---|
| Introduction to the tensor-programs framework, a PL approach that helps analyse ... | Hongseok Yang | 58m |
Introduces Greg Yang’s tensor‑programs framework: a simple straight-line tensor language that encodes forward and backward neural computations parameterized by… | ||
| Exact Inference for Discrete Probabilistic Programs via Generating Functions | Fabian Zaiser, C.-H. Luke Ong | 11m |
Exact inference method represents program state distributions with probability generating functions and transforms those closed-form PGFs across sampling… | ||
| Exact Probabilistic Inference Using Generating Functions | Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen | 14m |
Generative-function semantics represent discrete program distributions as formal power series and use multiplicative inverses to get closed-form fractions… | ||
| What do posterior distributions of probabilistic programs look like? | Mathieu Huot, Alexander K. Lew, Vikash K. Mansinghka, Sam Staton | 20m |
Defines s-Hausdorff measures and proves any probabilistic program with piecewise analytic primitives denotes a measure that has a density w.r.t. some… | ||
| Semantics of Probabilistic Program Traces | Alexander K. Lew, Eli Sennesh, Jan-Willem Van De Meent, Vikash K. Mansinghka | 18m |
Provides a minimal core calculus that models trace-based PPLs and a categorical account in quasi-Borel spaces that treats traces as measurable objects. Defines… | ||
| Random probability distributions as natural transformations | Victor Blanchi, Hugo Paquet | 04m |
Claim: homogeneous random distributions — where atom locations are independent of atom weights — bijectively correspond to natural transformations G -> GG for… | ||
| Static Delayed Sampling for Probabilistic Programming Languages | Gizem Caylak, Daniel Lundén, Viktor Senderov, David Broman | 06m |
Introduces static delayed sampling that moves delayed-sampling operations to compile time by constructing a programmatic Bayesian network, applying automated… | ||
| Denotational semantics of languages for inference: semirings, monads, and tensor... | Cristina Matache, Sean K. Moss, Sam Staton, Ariadne Si Suo | 05m |
Claims an explicit algebraic route: modules over a semiring R yield monads T_R sending X to finitely supported unnormalized measures R^X and submonads fixing… | ||
| Separated and Shared Effects in Higher-Order Languages | Justin Hsu | 04m |
Proposes two higher-order languages, λ^1_{INI} with a linear type system that distinguishes independent and possibly-dependent pairs, and λ^2_{INI}, a… | ||
| On Iteration in Discrete Probabilistic Programming | Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva, Fabio Zanasi | 05m |
Extends the discrete PPL dice with two concrete unbounded-iteration constructs and shows how exact inference still runs by compiling into binary decision… | ||
| Bit-Blasting Probabilistic Programs | Poorva Garg, Steven Holtzen, Guy Van den Broeck, Todd Millstein | 05m |
HyBit converts continuous variables into a discrete bitblasted representation by encoding each real as independent Bernoulli bits, then runs exact inference… | ||
| πMPC: Automatic Security Proofs for MPC Protocols | Mako P. Bates, Joseph P. Near | 05m |
A domain-specific language plus static analyzer aims to produce automatic simulator synthesis for secure multiparty computation by validating programs in two… | ||
| The Variable Elimination Algorithm as a Let-Term Rewriting | Thomas Ehrhard, Claudia Faggian, Michele Pagani | 19m |
Expresses variable elimination for Bayesian networks as let-term linear lambda-calculus rewriting and proves any VE factorization is reachable by four simple… | ||
| On the Reparameterisation Gradient for Non-Differentiable but Continuous Models | C.-H. Luke Ong, Dominik Wagner | 07m |
Claim: the reparameterisation gradient is unbiased for continuous but possibly non-differentiable probabilistic programs. Proof uses a categorical denotational… | ||
| Partial Evaluation of Forward-Mode Automatic Differentiation | Oscar Eriksson, Viktor Palmkvist, David Broman | 05m |
A whole-program transformation called PEAD (partial evaluation automatic differentiation) combines compile-time symbolic differentiation with forward-mode AD… | ||
| Distribution Theoretic Semantics for Non-Smooth Differentiable Programming | Christopher Lam | 06m |
Defines lambda_δ, a simply-typed core calculus that lifts arbitrary (even discontinuous) functions to distributions and gives a concrete semantics using… | ||
| New foundations for probabilistic separation logic | John Li, Amal Ahmed, Steven Holtzen | 05m |
Proposes a new separation-logic semantics where propositions are sets of probability spaces and heaps are replaced by probability-space fragments combined with… | ||
| Verified Reversible Programming for Verified Lossless Compression | James Townsend, Jan-Willem Van De Meent | 06m |
A tiny reversible language called Flipper is implemented as an Agda macro that compiles a single reversible codec function into an encoder, a decoder and… | ||
| Pitfalls of Full Bayesian Inference in Universal Probabilistic Programming | Tim Reichelt, C.-H. Luke Ong, Tom Rainforth | 06m |
Argues that full Bayes on universal PPLs treats programs as a Bayesian Model Average over their straight-line programs (SLPs), which can make posterior SLP… | ||
| Contextual source code AD transformations for sum types | Adam Paszke, Gordon Plotkin | 23m |
Provides context-based source-code transformations that implement forward AD, reverse AD and transposition for a first-order language with products and sums… | ||
| nothing matches | ||