Sessions
First-class Logical Refinement Types for Scala
Talk
13. October 2026, 11:20 - 11:50
Maschinenhaus
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.