Thu 27 Aug 2026 11:24 - 11:42 at IP126 Auditorium - Program Analysis Chair(s): Ben Greenman

We introduce a new programming language and its categorical semantics in order to design and implement neural networks within the framework of algebraic effects and handlers for arrows. Our language enables us to construct neural networks symbolically, in the same manner as algebraic effects, and to assign implementations—such as backpropagation computations—to them via handlers. The advantage of this language design is that network descriptions become abstract and high-level, while implementations can be flexibly assigned to networks. We establish a rigorous foundation for our language by developing a type system, an operational semantics, a categorical semantics, and soundness and adequacy theorems. The technical core is the introduction of \emph{reverse handlers}, a novel handler mechanism for arrows for implementing backpropagation, together with new algebras of strong promonads on reverse differential restriction categories (RDRCs), whose string diagrams provide a formal graphical syntax and semantics for neural networks.

Thu 27 Aug

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

10:48 - 12:00
Program AnalysisICFP Papers at IP126 Auditorium
Chair(s): Ben Greenman University of Utah
10:48
18m
Talk
Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
ICFP Papers
Zoe Paraskevopoulou National Technical University of Athens
DOI
11:06
18m
Talk
Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)Remote
ICFP Papers
Eleftherios Ioannidis Microsoft Research, Nikhil Swamy Microsoft Research, Gabriel Ebner Microsoft Research, Matthai Philipose Microsoft Research, Tahina Ramananandro Microsoft Research
DOI
11:24
18m
Talk
Programming Backpropagation with Reverse Handlers for Arrows
ICFP Papers
Takahiro Sanada Fukui Prefectural University, Keisuke Hoshino Research Institute for Mathematical Sciences, Kyoto University, Kenshin Hirai Research Institute for Mathematical Sciences, Kyoto University, Shin-ya Katsumata Kyoto Sangyo University
DOI
11:42
18m
Talk
On Recursion in Graded Modal Type Theory
ICFP Papers
Oskar Eriksson Department of Computer Science and Engineering, University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden, Andreas Abel Gothenburg University, Nils Anders Danielsson University of Gothenburg
DOI