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
Times are displayed in time zone: Tijuana, Baja California change

14:00 - 15:30
Session 4ARRAY at 106C
Chair(s): Tze Meng LowCMU
14:00
30m
Talk
TeIL: a type-safe imperative Tensor Intermediate Language
ARRAY
Norman A. RinkTU Dresden, Germany, Jeronimo CastrillonTU Dresden, Germany
14:30
30m
Talk
Records with Rank Polymorphism
ARRAY
A: Justin SlepakNortheastern University, A: Olin ShiversNortheastern University, USA, A: Panagiotis ManoliosNortheastern University
15:00
30m
Talk
Data-Parallel Flattening by Expansion
ARRAY
Martin ElsmanUniversity of Copenhagen, Denmark, Troels HenriksenUniversity of Copenhagen, Denmark, Niels G. W. SerupDIKU, University of Copenhagen