Daniel Urban

Research Engineer at Nokia Bell Labs

I'm a research engineer at Nokia Bell Labs, currently working on distributed systems with Scala. During this work, and sometimes in my free time, I occasionally contribute to open source Scala libraries (like shapeless or Cats).

Verifying state machine transitions with Scala types

While a lot of software systems implement and use finite-state machines, the correctness of the state transitions and operations is usually not statically verified. We present a Scala library, which allows defining statically verified domain-specific languages (DSLs) for working with state machines. Our library enables the compile-time checking of the implementation of these DSLs, by encoding states into Scala types, and using an indexed free monad and a type class for restricting state transitions.

Slides
Video ←Back