TL;DR
This tutorial explains how refinement types extend type systems with logical predicates to specify invariants, offering a flexible approach for ensuring software correctness through incremental language and type system enhancements.
Contribution
It provides a unified tutorial distilling key ideas and implementation strategies for modern refinement type systems from extensive literature.
Findings
Refinement types enable precise specification of invariants.
A step-by-step approach to implementing refinement type checkers.
Incremental language features facilitate understanding of refinement type systems.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
