Tue 19 Jun 2018 14:35 - 15:10 at Grand Ballroom C - Types and Correctness

Rank polymorphism serves as a type of control flow used in array-oriented languages, where functions are automatically lifted to operate on high-dimensional arguments. The iteration space is derived directly from the shape of the data, presenting a challenge to compilation. A type system can characterize data shape, though the level of detail is beyond what can be reasonably expected from entirely human-generated annotations. The task of checking or inferring shapes can be phrased as solving constraints in the theory of the free monoid over the natural numbers, but the constraints involve both universal and existential quantification. Here is a plan of attack for leveraging past work on decision procedures, which has generally focused on the purely existential fragment of the theory.

Tue 19 Jun
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

14:00 - 15:45: ARRAY 2018 - Types and Correctness at Grand Ballroom C
ARRAY-2018-papers14:00 - 14:35
Beatrice ÅkerblomStockholm University, Elias CastegrenUppsala University, Tobias WrigstadUppsala University
ARRAY-2018-papers14:35 - 15:10
Justin SlepakNortheastern University, Panagiotis ManoliosNortheastern University, Olin ShiversNortheastern University, USA
ARRAY-2018-papers15:10 - 15:45
Magne HaveraaenUniversity of Bergen, Norway