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

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