Title: Mechanising Tensors in Isabelle/HOL
Speakers: Filip Smola
Abstract:

In this talk I will describe our ongoing effort to mechanise tensors – a generalisation of scalars, vectors and matrices – in Isabelle/HOL. This project was started by Matt as part of his master’s project and builds on the work of Alexander Bentkamp (at that time of Vrije Universiteit Amsterdam).

I will introduce what tensors are and where they are used. They have found many uses around machine learning in particular, because they are good for expressing structured data and operations on it. Then I will introduce Bentkamp’s representation of tensors, highlight some of its drawbacks and show how our approach fixes those. Particularly interesting is the system we use to avoid having to redefine existing operations. Then I will close on some of our plans for to where take this project in the future.