Practical range refinement types with inference
Valentin Aebi and Carlo A. Furia - SEFM 2026
[PDF] [arXiv] [implementation] [replication package]

We introduce Ranger, a type system oriented towards lightweight verification using refinement types and dependent integer range types. Ranger's distinctive feature is its low annotation overhead thanks to bidirectional type inference supported by specialized heuristics for refinements inference. We implemented Ranger as part of the type system of the Licorne programming language, and show how its structured SSA intermediate representation helps supporting refinements on local variables updated in loops. We evaluate Ranger by comparing its expressiveness and annotation overhead to other lightweight verification frameworks and to the Scala language.