Scale By the Bay
Thursday, October 28, 2021
-
PDT
Shape safety in tensor programming is easy for a theorem prover
We present shapesafe (https://github.com/tribbloid/shapesafe) - the most comprehensive compile-time verifier for scala linear algebra - by only exploiting scala's type system as a theorem prover. This new paradigm allows type-level tensor computations, even those as complex as composite neural network blocks, to be rewritten, simplified and verified while being written. We will talk about its design and limitations, and most important, what we have observed and learned from it
Download these images to your phone and post using the Instagram app.