Contextual source code AD transformations for sum types (LAFI 2023) - POPL 2023

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

Who

Adam Paszke, Gordon Plotkin

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 14:20 - 14:40 at Scollay - Third Session Chair(s): Steven Holtzen, Christine Tasson

Abstract

We provide context-based source code transformations (SCTs) for the automatic differentiation of a simple first-order language with basic, product, and sum types. We consider and relate forward differentiation, reverse differentiation, and transposition SCTs. These SCTs are efficient (indeed they are straightforward structural recursions) and we give runtime and space efficiency bounds for the codes they produce. The target language of the SCTs is a first-order mixed linear/non-linear language. The tangent space of an element of a sum type (eg, real^2 + real^3) depends on which component of the type it inhabits. For that reason, the linear language has dependent types; in this we follow ideas of Lucatelli and Vakar.

File attachments

Contextual source code AD transformations for sum types (AD-transformations.pdf)	207KiB

Adam Paszke

Google Research

Poland

Gordon PlotkinAuthor

Google

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

	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