2015/07/01 by Niki Vazou, Vazou, Niki, Alexander Bakst +3 · 1 voice · 1 citation
Computer Science · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Security and Verification in Computing #cs.PL #cs.SE
paper · pdf · doi:10.48550/arxiv.1507.00385
openalex publication_date 2015/07/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.