Skip to main content
Open Access Publications from the University of California

UC Santa Cruz

UC Santa Cruz Electronic Theses and Dissertations bannerUC Santa Cruz

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.

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View