Matt Bovel
Matt Bovel is a PhD student at EPFL, where he works on type systems and program verification across two labs: the LAMP, led by Martin Odersky, and the LARA, led by Viktor Kunčak.
Session
10-13
11:20
30min
First-class Logical Refinement Types for Scala
Matt Bovel
What if assertions such as x > 0 were part of the type system? We present a prototype implementation of logical refinement types for Scala: types like {x: Int | x > 0}. In our system, refinement types are first-class: they can be nested, used as type arguments, and related by subtyping. We demonstrate the system through concrete examples.
Maschinenhaus
