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

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