.png){kind=icon}
.png){kind=icon}
Return
Refinement Types: A Tutorial
.png){kind=icon}
OA
AI
DOI：10.1561/2500000032.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
POLYMORPHISM
TERMINATION
STATE
Journal
F
IF:
0.5
Papers:
8
Citations:
130
