Bounded Refinement Types
This work addresses expressiveness limitations in refinement typing for developers and researchers in programming languages and verification, representing a significant but incremental advance.
The paper tackles the problem of limited expressiveness in refinement types by introducing bounded quantification, which enables typed combinators for relational algebra, Floyd-Hoare logic, and a refined IO monad with capability tracking. This approach retains automated SMT-based checking and inference, making refinement typing more practical.
We present a notion of bounded quantification for refinement types and show how it expands the expressiveness of refinement typing by using it to develop typed combinators for: (1) relational algebra and safe database access, (2) Floyd-Hoare logic within a state transformer monad equipped with combinators for branching and looping, and (3) using the above to implement a refined IO monad that tracks capabilities and resource usage. This leap in expressiveness comes via a translation to "ghost" functions, which lets us retain the automated and decidable SMT based checking and inference that makes refinement typing effective in practice.