Name
Abstract | ||
|---|---|---|
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type. These refinement predicates provide software developers a tunable knob with which to inform the type system about what invariants and correctness properties should be checked on their code, and give the type checker a way to enforce those properties at compile time. 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1561/2500000032 | FOUNDATIONS AND TRENDS IN PROGRAMMING LANGUAGES |
DocType | Volume | Issue |
Journal | 6 | 3-4 |
ISSN | Citations | PageRank |
2325-1107 | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ranjit Jhala | 1 | 2183 | 111.68 |
| Niki Vazou | 2 | 88 | 8.90 |