Proving Algebraic Laws in Scala using Stainless

[tobal]

speaker: Viktor Kunčak
topic: Scala, proving correctness
video: https://www.youtube.com/watch?v=dkO59PTcNxA
length: 1:03:29

Lambda Days 2020

Keynote: Proving Algebraic Laws in Scala using Stainless

I will give an overview of Stainless (https://stainless.epfl.ch).
Developers can use stainless to state and formally verify properties of functional programs written in Scala. I present foundation of stainless and its termination checks through an untyped functional language on top of which we impose a new type system, System FR. As an example of use case, I present how to build and develop verified hierarchy of algebraic structures, where Stainless proves laws when structures are instantiated.