Matt Bovel, Viktor Kunčak and Martin Odersky
OOPSLA 2026
Paper (latest) Paper (ACM) DOI arXiv Slides Playground Mechanization Repo
Refinement types—types qualified with logical predicates—have proven effective for lightweight verification in languages like Liquid Haskell, F*, and Dafny. However, in these systems refinements are either written in a separate specification language or treated as second-class annotations, disconnected from the host language's type system. This disconnect creates usability barriers: programmers must maintain two mental models, and refinements cannot interact with features like type inference, subtyping, or overloading.
We present the design of first-class refinement types for Scala 3, where refinements are ordinary types that participate in subtyping, inference, and pattern matching alongside existing language features. We prove type soundness of a core, pure calculus mechanized in Rocq, combining dependent function types, bounded polymorphism, positive equi-recursive types, union and intersection types, and refinement types, using a fuel-bounded definitional interpreter and semantic typing. A distinctive design choice is our partial-correctness semantics: predicates are arbitrary terms that may diverge, and type soundness requires no termination assumptions. Finally, we implement our design as a prototype extension of the Scala 3 compiler with a lightweight e-graph-based solver for predicate entailment.
paper.pdf is the current version, rebuilt from the LaTeX sources in the repository and including any corrections made since publication.
paper-acm.pdf is the version of record, published open access under CC BY 4.0 as Proc. ACM Program. Lang. 10(OOPSLA2), article 409, and carrying the artifact evaluation badges.
Slides for the OOPSLA 2026 talk, as reveal.js slides or as a PDF.
The playground type-checks Scala code against the prototype in the browser, with no installation. Programs are compiled on a server running the implementation.
A prototype extension of the Scala 3 compiler, enabled with
-language:experimental.qualifiedTypes. It lives on the
refinement-types
branch of epfl-lara/dotty; upstream pull request:
scala/scala3#21586.
The soundness proof in Rocq, browsable as rendered Rocq documentation.
Compilation-time benchmarks comparing our implementation with Stainless and with Georg Schmid's 2016 LiquidTyper, plus the script that generates the paper's results table.
All three components, together with the paper's LaTeX sources and a Docker image that reproduces the results, are in the project's repository.