Executable Refinement Types

This dissertation introduces executable refinement types, a type system with the expressivity of program contracts, and establishes their metatheory and accompanying implementation techniques. To enforce them, we introduce Hybrid Type Checking which combines best-effort static checking with dynamic checking. We propose a novel definition of type reconstruction and show that it is decidable even though type checking is not. Then, we show how compositional reasoning is key to predictability of checking, and how to restore it to dependent types. Finally, we explore architectural ideas by implementing Executable Refinement Types in our language Sage, where the dynamic checks feed back into static checks such that every dynamic failure occurs at most once