Expressive Reachability Types with Sound and Decidable Bidirectional Type Checking

The authors present the 휆q 푅-calculus, a refined calculus for reachability types that addresses key limitations in prior work by introducing a more expressive subtyping relation and a sound and decidable bidirectional type checking algorithm.