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: (GMT-07:00) Tijuana, Baja California change

14:00 - 15:30: ARRAY 2019 - Session 4 at 106C
Chair(s): Tze Meng LowCMU
ARRAY-2019-papers14:00 - 14:30
Norman A. RinkTU Dresden, Germany, Jeronimo CastrillonTU Dresden, Germany
ARRAY-2019-papers14:30 - 15:00
Justin SlepakNortheastern University, Olin ShiversNortheastern University, USA, Panagiotis ManoliosNortheastern University
ARRAY-2019-papers15:00 - 15:30
Martin ElsmanUniversity of Copenhagen, Denmark, Troels HenriksenUniversity of Copenhagen, Denmark, Niels G. W. SerupDIKU, University of Copenhagen