Day 4 -
Aug 21st
Creative and Mix
Scala, because of its functional nature, already gives us some design tools to write correct programs: type polymorphism, higher-order functions, immutability, and others. There are also many test frameworks that allow us to detect some bugs. This is a good start, but we can do more: proving the absence of bugs. In this talk I will show how to use Isabelle, a proof assistant, to implement algorithms, prove them correct, and compile them as Scala programs. We’ll see how to formulate universal properties on programs and how to check them.
Giesecke+Devrient
Lars is an Evangelist at Giesecke+Devrient, a security technology company. An engineer at heart, they are working to bring modern financial services to people. Lars writes articles and talks about a multitude of topics. Previously, Lars was a PhD student at TU München in the field of logic and verification. Their research focus was on techniques for verified code generation from theorem provers.
Subscribe and follow @ScalaDays on BlueSky for the latest conference updates.