Bounded Refinement Types

TL;DR

This paper introduces bounded quantification for refinement types, significantly enhancing their expressiveness to model relational algebra, logic, and resource tracking while maintaining automated SMT-based verification.

Contribution

It develops a novel bounded quantification approach for refinement types, enabling advanced applications like database access, logic, and resource management with automated checking.

Findings

Enhanced expressiveness of refinement types through bounded quantification

Successful modeling of relational algebra and database access

Implementation of resource-aware IO monad with automated verification

Abstract

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.