Fri 19 Jun 2026 11:20 - 11:40 at Flatirons 3 - Verified Compilation and Type Systems Chair(s): Charles Yuan

Discrete structures are currently second-class in differentiable programming. Since functions over discrete structures lack overt derivatives, differentiable programs do not differentiate through them and limit where they can be used. For example, when programming a neural network, conditionals and iteration cannot be used everywhere; they can break the derivatives necessary for gradient-based learning to work. This limits the class of differentiable algorithms we can directly express, imposing restraints on how we build neural networks and differentiable programs more generally. However, these restraints are not fundamental. Recent work shows conditionals can be first-class, by compiling them into differentiable form as linear neurons. Similarly, this work shows iteration can be first-class—by compiling to linear recurrent neurons. We present a minimal typed, higher-order and linear programming language with iteration called Cajal(N). We prove its programs compile correctly to recurrent neurons, allowing discrete algorithms to be expressed in a differentiable form compatible with gradient-based learning. With our implementation, we conduct two experiments where we link these recurrent neurons against a neural network solving an iterative image transformation task. This determines part of its function prior to learning. As a result, the network learns faster and with greater data-efficiency relative to a neural network programmed without first-class iteration. A key lesson is that recurrent neurons enable a rich interplay between learning and the discrete structures of ordinary programming.

Fri 19 Jun

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

11:00 - 12:40
Verified Compilation and Type SystemsPLDI Research Papers at Flatirons 3
Chair(s): Charles Yuan University of Wisconsin-Madison
11:00
20m
Talk
Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
PLDI Research Papers
Zhengyao Lin Carnegie Mellon University, Yi Cai University of Maryland at College Park, Milijana Surbatovich University of Maryland at College Park
DOI
11:20
20m
Talk
Compiling to Recurrent Neurons
PLDI Research Papers
Joey Velez-Ginorio University of Pennsylvania, Nada Amin Harvard University, Konrad Kording University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI
11:40
20m
Talk
[TOPLAS] Denotation-based Compositional Compiler Verification
PLDI Research Papers
Zhang Cheng Shanghai Jiao Tong University, Jiyang Wu , Di Wang Peking University, Qinxiang Cao Shanghai Jiao Tong University
12:00
20m
Talk
Responsive Parallelism with Dynamic and First-Class Priorities
PLDI Research Papers
Marelle León Illinois Institute of Technology, My Dinh Illinois Institute of Technology, Stefan K. Muller University of Connecticut
DOI
12:20
20m
Talk
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
PLDI Research Papers
Songlin Jia Purdue University, Guannan Wei Tufts University, Siyuan He Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University
DOI