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 AugDisplayed time zone: Eastern Time (US & Canada) change
10:48 - 12:00 | |||
10:48 18mTalk | Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report) ICFP Papers Zoe Paraskevopoulou National Technical University of Athens DOI | ||
11:06 18mTalk | 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 18mTalk | 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 18mTalk | 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 | ||