This program is tentative and subject to change.
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, interpreting arrays as positive types requires the introduction of variables with multiplicity. We follow a similar approach for Booleans by introducing conditionally-defined variables.
The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (AiNF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. AiNF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to AiNF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.
This program is tentative and subject to change.
Mon 16 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | |||
10:30 15mTalk | Static Basic Block Versioning Technical Papers Manuel Serrano Inria; University of Côte d'Azur, Olivier Melançon Université de Montréal, Marc Feeley Université de Montréal | ||
10:45 15mTalk | Cross Module Quickening - The Curious Case of C Extensions Technical Papers Felix Berlakovich μCSRL, CODE Research Institute, University of the Bundeswehr Munich, Stefan Brunthaler Bundeswehr University Munich | ||
11:00 15mTalk | Compiling with Arrays Technical Papers David Richter Technical University of Darmstadt, Timon Böhler Technical University of Darmstadt, Pascal Weisenburger University of St. Gallen, Mira Mezini TU Darmstadt Pre-print | ||
11:15 15mTalk | The Performance Effects of Virtual-Machine Instruction Pointer Updates Technical Papers | ||
11:30 15mTalk | Taking a Closer Look: An Outlier-Driven Approach to Compilation-Time Optimization Technical Papers Florian Huemer JKU Linz, David Leopoldseder Oracle Labs, Aleksandar Prokopec Oracle Labs, Raphael Mosaner JKU Linz, Hanspeter Mössenböck JKU Linz | ||
11:45 15mTalk | Optimizing Layout of Recursive Datatypes with Marmoset Technical Papers Vidush Singhal Purdue University, Chaitanya S. Koparkar Indiana University, Joseph Zullo Purdue University, Artem Pelenitsyn Purdue University, Michael Vollmer University of Kent, Mike Rainey Carnegie Mellon University, Ryan R. Newton Purdue University, Milind Kulkarni Purdue University Pre-print |