Refinement Types: A Tutorial
This is an incremental tutorial aimed at software developers and researchers interested in learning about refinement types for improving code verification.
The paper provides a tutorial on refinement types, which enhance type systems with logical predicates to check code invariants and correctness properties, by explaining key concepts and demonstrating implementation through a series of progressively enhanced languages.
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what invariants and correctness properties should be checked on their code. In this article, we distill the ideas developed in the substantial literature on refinement types into a unified tutorial that explains the key ingredients of modern refinement type systems. In particular, we show how to implement a refinement type checker via a progression of languages that incrementally add features to the language or type system.