Sat 22 Jun 2019 14:00 - 14:30 at 106C - Session 4 Chair(s): Tze Meng Low

Each of the popular tensor frameworks from the machine learning domain comes with its own language for expressing tensor kernels. Since these tensor languages lack precise specifications, it is impossible to understand and reason about tensor kernels that exhibit unexpected behaviour. In this paper, we give examples of such kernels. The tensor languages are superficially similar to the well-known functional array languages, for which formal definitions often exist. However, the tensor languages are inherently imperative. In this paper we present TeIL, an imperative tensor intermediate language with precise formal semantics. For the popular tensor languages, TeIL can serve as a common ground on the basis of which precise reasoning about kernels becomes possible. Based on TeIL’s formal semantics we develop a type-safety result in the Coq proof assistant.

Sat 22 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
Session 4ARRAY at 106C
Chair(s): Tze Meng Low CMU
14:00
30m
Talk
TeIL: a type-safe imperative Tensor Intermediate Language
ARRAY
Norman A. Rink TU Dresden, Germany, Jeronimo Castrillon TU Dresden, Germany
14:30
30m
Talk
Records with Rank Polymorphism
ARRAY
A: Justin Slepak Northeastern University, A: Olin Shivers Northeastern University, USA, A: Panagiotis Manolios Northeastern University
15:00
30m
Talk
Data-Parallel Flattening by Expansion
ARRAY
Martin Elsman University of Copenhagen, Denmark, Troels Henriksen University of Copenhagen, Denmark, Niels G. W. Serup DIKU, University of Copenhagen